
Boogie
 Referenced in 120 articles
[sw07714]
 conditions that are passed to an SMT solver. The default SMT solver...

Yices
 Referenced in 157 articles
[sw04436]
 Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted...

VeriFast
 Referenced in 66 articles
[sw07705]
 about the primitive recursive functions. An SMT solver is used to solve queries over data ... that prevents nontermination of the SMT solver while enabling reduction of any ground term ... either the verifier or the SMT solver, verification time is predictable...

MathSAT
 Referenced in 61 articles
[sw09449]
 MathSAT 4 SMT Solver. We present MathSAT 4, a stateoftheart SMT solver ... provides functionalities which extend the applicability of SMT in this setting. In particular: model generation...

MathSAT5
 Referenced in 56 articles
[sw09569]
 mathsat5 SMT solver. MathSAT is a longterm project, which has been jointly carried ... maintaining a stateoftheart SMT tool for formal verification (and other applications). MathSAT5 ... SMT formulae; finally, a framework allowing users for plugging their custom tuned SAT solvers. MathSAT5...

dReal
 Referenced in 34 articles
[sw07157]
 dReal: an SMT solver for nonlinear theories over the reals. We describe the opensource ... tool dReal, an SMT solver for nonlinear formulas over the reals. The tool can handle...

Boolector
 Referenced in 32 articles
[sw00085]
 Boolector: an efficient SMT solver for bitvectors and arrays. Satisfiability Modulo Theories ... Boolector, which is an efficient SMT solver for the quantifierfree theories of bitvectors...

veriT
 Referenced in 31 articles
[sw07281]
 veriT: An Open, Trustable and Efficient SMTSolver. This article describes the first public version ... satisfiability modulo theory (SMT) solver veriT. It is opensource, proofproducing, and complete...

EasyCrypt
 Referenced in 33 articles
[sw09738]
 checked automatically using offtheshelf SMT solvers and automated theorem provers, and then compiled...

OpenSMT
 Referenced in 28 articles
[sw08426]
 incremental, efficient, and opensource SMTsolver. OpenSMT has been specifically designed to be easily...

SMTRAT
 Referenced in 19 articles
[sw13091]
 combined to (1) an SMT solver or (2) a theory solver in order to extend ... supported logics of an existing SMT solver by the supported logics of SMTRAT. Further...

SYMBA
 Referenced in 13 articles
[sw08528]
 Symbolic optimization with SMT solvers. The rise in efficiency of Satisfiability Modulo Theories (SMT) solvers ... these applications, SMT solvers are used for generating satisfying assignments (e.g., a witness ... calls. Unfortunately, none of the available SMT solvers offer such optimization capabilities. In this paper ... value of t. SYMBA utilizes efficient SMT solvers as black boxes. As a result...

SMTInterpol
 Referenced in 22 articles
[sw07406]
 SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. The solver...

vZ
 Referenced in 14 articles
[sw22666]
 Optimizing SMT Solver. νZ is a part of the SMT solver Z3. It allows users ... approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations. Objective functions ... that allows dispatching problems to special purpose solvers, and examine use cases...

Reluplex
 Referenced in 20 articles
[sw31367]
 Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. Deep neural networks have emerged...

dReach
 Referenced in 19 articles
[sw20164]
 deltadecision procedures in the SMT solver dReach. In this way, dReach is able...

Norn
 Referenced in 10 articles
[sw21853]
 Norn: an SMT solver for string constraints. We present version 1.0 of the Norn ... SMT solver for string constraints. Norn is a solver for an expressive constraint language, including ... feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption...

LLBMC
 Referenced in 16 articles
[sw09478]
 bounded model checking using an SMT solver and thus achieves bitaccurate precision. A distinguishing...

WoLFram
 Referenced in 15 articles
[sw02075]
 software. It is shown, that modern SAT solvers can formally verify PLC programs within ... Boolean SAT engine with an SMT solver is an option to cope with the complexity...

Beaver
 Referenced in 10 articles
[sw00071]
 Beaver: Engineering an efficient SMT solver for bitvector arithmetic. Beaver is an SMT solver ... operators. Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich...