Introduction

Decision procedures for checking satisfiability of logical formulas are crucial for many verification applications. Of particular recent interest are solvers for Satisfiability Modulo Theories (SMT). SMT solvers decide logical satisfiability (or dually, validity) with respect to a background theory expressed in classical first-order logic with equality. The success of SMT for verification applications is largely due to the suitability of supported background theories for expressing verification conditions. These theories include:

• the empty theory, which gives rise to the so-called logic of equality and uninterpreted functions (EUF).
• real or integer arithmetic
• theories of program or hardware structures such as bitvectors, arrays, and recursive datatypes.

It is usually necessary to adopt some syntactic restriction on the input formulas to be checked in order to ensure efficient decidability. For example, formulas are often required to be quantifier-free. For arithmetic, more efficient algorithms are known for difference formulas, where atomic formulas consist just of difference constraints of the form x - y <= c, with x and y variables and c a numeric constant. Many solvers further increase expressivity by taking the background theory to be a combination of several individual theories, and some solvers include limited support for user-supplied quantified axioms, further increasing expressive power.

Public competitions are a well-known means of stimulating advancement in software tools. For example, in automated reasoning, the CASC competition for first-order reasoning tools has seen steady improvement in the systems entered since the competition began in 1996. The SAT competition for propositional SAT solvers has also seen similar, sometimes dramatic, improvements from year to year. Exactly what role the competitions play in these improvements is hard to measure, but anecdotal evidence suggests that they act as a significant catalyst for tool implementors.

The idea of holding SMT-COMP came out of discussions surrounding the SMT-LIB initiative at the 2nd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR) at IJCAR 2004. SMT-LIB is an initiative of the SMT community to build a library of SMT benchmarks in a proposed standard format. SMT-COMP will help serve this goal by contributing collected benchmark formulas used for the competition to the library, and by providing an incentive for implementors of SMT solvers to support the SMT-LIB format.

Last modified: Tue 17 Feb 2015 14:59 UTC