• VeriFast

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

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

• Mcmt

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

• PAGAI

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

• TACO

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

• vZ

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

• VeriMAP

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

• 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 13 articles [sw20164]
• numbers, which are solved by delta-decision procedures in the SMT solver dReach. In this...

• InvA

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

• JavaSMT

• Referenced in 1 article [sw18525]
• newly developed tools rely on SMT solving. The SMT-LIB initiative defines a common format ... solver-independent API layer for SMT solving. Our library aims to close the gap between...

• Clingcon

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

• smt

• Referenced in 14 articles [sw09205]
• arithmetic operators and functions on them. The smt toolbox for Matlab introduces two new classes ... toolbox new routines for solving Toeplitz linear systems. (netlib numeralgo na30...