- Referenced in 182 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 104 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 116 articles
- verification conditions that are passed to an SMT solver. The default SMT solver...
- Referenced in 138 articles
- Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted...
- Referenced in 84 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 57 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
- 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 44 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 27 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 29 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 26 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 36 articles
- adopts state-of-the-art techniques from SMT and uses conflict-driven learning and theory...
- Referenced in 17 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 21 articles
- points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques, efficient heuristics...
- Referenced in 28 articles
- OpenSMT, an incremental, efficient, and open-source SMT-solver. OpenSMT has been specifically designed...
- Referenced in 28 articles
- checked automatically using off-the-shelf SMT solvers and automated theorem provers, and then compiled...
- Referenced in 19 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 24 articles
- language models. In addition to the SMT decoder, the toolkit also includes a wide variety...
- Referenced in 14 articles
- smt: A Matlab toolbox for structured matrices. The full exploitation of the structure of large ... arithmetic operators and functions on them. The smt toolbox for Matlab introduces two new classes...
- Referenced in 11 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...