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

SMTRAT
 Referenced in 18 articles
[sw13091]
 toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations ... methods for solving quantifierfree (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 quantifierfree ... operators. Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich...

Mcmt
 Referenced in 21 articles
[sw11911]
 safety and fixpoints by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques...

CalCS
 Referenced in 7 articles
[sw13098]
 CalCS: SMT solving for nonlinear convex constraints. Certain formal verification tasks require reasoning about ... present a new technique for satisfiability solving of Boolean combinations of nonlinear 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 (SMTsolving), focusing on distinction of paths inside...

TACO
 Referenced in 6 articles
[sw07668]
 solving, model checking or SMTsolving...

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

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 SMTLIB format (.smt2) (including...

ac2lus
 Referenced in 2 articles
[sw17953]
 ac2lus: Bringing SMTsolving and Abstract Interpretation Techniques to RealTime Calculus through the Synchronous ... allowing the use of techniques like SMTsolving 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 deltadecision procedures in the SMT solver dReach. In this...

InvA
 Referenced in 2 articles
[sw10124]
 narrowing, equationallydefined 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 SMTLIB initiative defines a common format ... solverindependent 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 nonlinear finite integers ... adopts stateoftheart techniques from SMT and uses conflictdriven 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...