- Referenced in 196 articles
- SMT-LIB was created with the expectation that the availability of common standards ... facilitate the evaluation and the comparison of SMT systems, and advance the state...
- Referenced in 125 articles
- automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove ... support the features of CVC3 and SMT-LIBv2 while optimizing the design of the core ... intended to be an open and extensible SMT engine, and it can be used...
- Referenced in 120 articles
- verification conditions that are passed to an SMT solver. The default SMT solver...
- Referenced in 157 articles
- Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted...
- Referenced in 86 articles
- automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. CVC3 is the last offspring ... series of popular SMT provers, which originated at Stanford University with the SVC system...
- Referenced in 66 articles
- facts about the primitive recursive functions. An SMT solver is used to solve queries over ... described that prevents non-termination of the SMT solver while enabling reduction of any ground ... performed by either the verifier or the SMT solver, verification time is predictable...
- Referenced in 56 articles
- mathsat5 SMT solver. MathSAT is a long-term project, which has been jointly carried ... maintaining a state-of-the-art SMT tool for formal verification (and other applications). MathSAT5 ... tool. It supports most of the SMT-LIB theories and their combinations, and provides many ... improved incrementality support, which is vital in SMT applications; second, a full support...
- Referenced in 61 articles
- MathSAT 4 SMT Solver. We present MathSAT 4, a state-of-the-art SMT solver ... provides functionalities which extend the applicability of SMT in this setting. In particular: model generation...
- Referenced in 32 articles
- Boolector: an efficient SMT solver for bit-vectors and arrays. Satisfiability Modulo Theories ... SMT) is the problem of deciding satisfiability of a logical formula, expressed in a combination ... features of Boolector, which is an efficient SMT solver for the quantifier-free theories...
- Referenced in 34 articles
- dReal: an SMT solver for nonlinear theories over the reals. We describe the open-source ... tool dReal, an SMT solver for nonlinear formulas over the reals. The tool can handle...
- Referenced in 31 articles
- veriT: An Open, Trustable and Efficient SMT-Solver. This article describes the first public version ... satisfiability modulo theory (SMT) solver veriT. It is open-source, proof-producing, and complete...
- Referenced in 39 articles
- adopts state-of-the-art techniques from SMT and uses conflict-driven learning and theory...
- Referenced in 19 articles
- SMT-RAT is an open source C++ toolbox for strategic and parallel SMT solving consisting ... collection of SMT compliant implementations of methods for solving quantifier-free (non)linear real ... modules can be combined to (1) an SMT solver or (2) a theory solver ... extend the supported logics of an existing SMT solver by the supported logics...
- Referenced in 24 articles
- points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques, efficient heuristics...
- Referenced in 33 articles
- checked automatically using off-the-shelf SMT solvers and automated theorem provers, and then compiled...
- Referenced in 20 articles
- puts together the automation of an SMT-backed deductive verification tool with the expressive power ... meet their specifications using a combination of SMT solving and interactive proofs...
- Referenced in 28 articles
- OpenSMT, an incremental, efficient, and open-source SMT-solver. OpenSMT has been specifically designed...
- Referenced in 28 articles
- Integers and Reals, and it provides advanced SMT-based model checking techniques. Besides extended functionalities...
- Referenced in 13 articles
- Symbolic optimization with SMT solvers. The rise in efficiency of Satisfiability Modulo Theories (SMT) solvers ... types, etc. In all of these applications, SMT solvers are used for generating satisfying assignments ... calls. Unfortunately, none of the available SMT solvers offer such optimization capabilities. In this paper ... present SYMBA, an efficient SMT-based optimization algorithm for objective functions in the theory...
- Referenced in 18 articles
- training data for statistical machine translation (SMT). We trained SMT systems for 110 language pairs...