OpenSMT

As a part of research on decision procedures, our Lab develops a tool, OpenSMT, that is used as a framework to perform all our experiments.

OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine of formal verification. OpenSMT is built on top of MiniSAT (http://minisat.se).

OpenSMT supports the following theories:

• QF_UF — Theory of Equality and Uninterpreted Functions
• QF_IDL — Theory of Differences on the Integers
• QF_RDL — Theory of Differences on the Rationals
• QF_LRA — Theory of Linear Arithmetic on the Rationals
• QF_BV — Theory of Fixed-Width Bit Vectors
• QF_UFIDL — Theory combination of Uninterpreted Functions and Differences on the Integers
• QF_UFLRA — Theory combination of Uninterpreted Functions and Linear Arithmetic on the Rationals

We encourage other researchers to build their algorithms for SMT solving in the OpenSMT framework. For that we dramatically simplified the process of building/customizing the solver - see "Build your solver" tutorial.

OpenSMT is currently released under the GNU General Public Licence version 3. Code is available via SVN at http://code.google.com/p/opensmt/. It compiles on 32 and 64 bits architectures.

OpenSMT participated the SMTCOMP'08 and SMTCOMP'09. Although not yet as fast as other industrial systems, OpenSMT is currently the fastest open-source SMT Solver for QF_UF, QF_IDL, QF_RDL, QF_LRA theories.

A general system description can be found here; for other references, please check the attachments below.