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

Mjollnir
 Referenced in 14 articles
[sw38338]
 nested lazy model enumeration through SMTsolving, 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 quantifierfree ... 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 fixpoints by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques...

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

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

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

SmtSwitch
 Referenced in 2 articles
[sw41581]
 solveragnostic C++ API for SMT solving. This paper presents SmtSwitch, an opensource ... solveragnostic API for SMT solving. SmtSwitch provides simple, uniform, and highperformance 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 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...

dReach
 Referenced in 18 articles
[sw20164]
 numbers, which are solved by deltadecision 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 realworld floatingpoint code. Solving floatingpoint constraints ... SMT solvers still often run into difficulties when solving complex, nonlinear floatingpoint constraints ... paper proposes a new approach to SMT solving that does not need to directly reason ... floatingpoint satisfiability to MO, and (2) solves the latter via the Monte Carlo Markov...