Results 1 to 20 of 175
Sort by:

  • VeriFast
  • Referenced in 59 articles [sw07705]
  • primitive recursive functions. An SMT solver is used to solve queries over data values ... described that prevents non-termination of the SMT solver while enabling reduction of any ground...

  • SMT-RAT
  • Referenced in 18 articles [sw13091]
  • toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations ... methods for solving quantifier-free (non)linear real and integer arithmetic ... modules can be combined to (1) an SMT solver or (2) a theory solver...

  • F*
  • Referenced in 20 articles [sw27563]
  • their specifications using a combination of SMT solving and interactive proofs...

  • Mjollnir
  • Referenced in 14 articles [sw38338]
  • nested lazy model enumeration through SMT-solving, and projections. This scheme may be applied...

  • Beaver
  • Referenced in 9 articles [sw00071]
  • vector arithmetic. Beaver is an SMT solver (theorem prover) for the theory of quantifier-free ... operators. Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich...

  • TACO
  • Referenced in 7 articles [sw07668]
  • solving, model checking, or SMT-solving...

  • Mcmt
  • Referenced in 22 articles [sw11911]
  • safety and fix-points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques...

  • CalCS
  • Referenced in 7 articles [sw13098]
  • CalCS: SMT solving for non-linear convex constraints. Certain formal verification tasks require reasoning about ... present a new technique for satisfiability solving of Boolean combinations of non-linear constraints that ... programming to realize a satisfiability modulo theory (SMT) solver. Our solver, CalCS, uses a lazy...

  • VeriMAP
  • Referenced in 7 articles [sw22866]
  • fields of constraint logic programming and SMT solving...

  • PAGAI
  • Referenced in 7 articles [sw13095]
  • combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside...

  • vZ
  • Referenced in 11 articles [sw22666]
  • users to pose and solve optimization problems modulo theories. Many SMT applications use models ... portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations...

  • NLambda
  • Referenced in 5 articles [sw23172]
  • about the language in an article: ’SMT Solving for Functional Programming over Infinite Structures...

  • Psyche
  • Referenced in 5 articles [sw28518]
  • illustrate Psyche by using it for SMT-solving...

  • raSAT
  • Referenced in 8 articles [sw15206]
  • Real numbers. raSAT is an SMT to solve problems in QF_NRA category, i.e., bounded ... raSAT is based on an interval constraint solving, similar to HySAT. raSAT prepares various interval ... linux. raSAT accepts inequality problems in SMT-LIB format (.smt2) (including...

  • ac2lus
  • Referenced in 2 articles [sw17953]
  • ac2lus: Bringing SMT-solving and Abstract Interpretation Techniques to Real-Time Calculus through the Synchronous ... allowing the use of techniques like SMT-solving and abstract interpretation which were not previously...

  • TSAT++
  • Referenced in 3 articles [sw21350]
  • based approach to satisfiability modulo theories (SMT). SMT is the problem of determining satisfiability ... satisfiability checker cooperate in order to solve SMT. Modularity allows both different enumerators, and satisfiability...

  • dReach
  • Referenced in 16 articles [sw20164]
  • numbers, which are solved by delta-decision procedures in the SMT solver dReach. In this...

  • XSat
  • Referenced in 2 articles [sw26290]
  • hurdle in applying SMT techniques to real-world floating-point code. Solving floating-point constraints ... SMT solvers still often run into difficulties when solving complex, non-linear floating-point constraints ... paper proposes a new approach to SMT solving that does not need to directly reason ... floating-point satisfiability to MO, and (2) solves the latter via the Monte Carlo Markov...

  • Clingcon
  • Referenced in 38 articles [sw09892]
  • Answer Set Programming (ASP) with constraint solving. Constraints over non-linear finite integers ... adopts state-of-the-art techniques from SMT and uses conflict-driven learning and theory...

  • InvA
  • Referenced in 2 articles [sw10124]
  • narrowing, equationally-defined equality predicates, and SMT solving, InvA achieves a significant degree of automation...