• VeriFast

• Referenced in 64 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 19 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 10 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...

• VeriMAP

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

• Mcmt

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

• TACO

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

• vZ

• Referenced in 12 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...

• 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...

• PAGAI

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

• NLambda

• Referenced in 6 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...

• Smt-Switch

• Referenced in 2 articles [sw41581]
• solver-agnostic C++ API for SMT solving. This paper presents Smt-Switch, an open-source ... solver-agnostic API for SMT solving. Smt-Switch provides simple, uniform, and high-performance access ... SMT solving for applications in areas such as automated reasoning, planning, and formal verification ... interface, which can be implemented by different SMT solvers. The interface allows the user...

• 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...

• dReach

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

• 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...

• PySMT

• Referenced in 5 articles [sw19843]
• algorithms. pySMT: A library for SMT formulae manipulation and solving http://www.pysmt.org. pySMT: a Python ... SMT: pySMT makes working with Satisfiability Modulo Theory simple: Define formulae in a simple, intuitive ... Solve your formulae using one of the native solvers, or by wrapping any SMT...

• 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...