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.

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 first SMT-COMP was held July 6-8, 2005, as a satellite event of CAV'05 first three days of the conference, with results updated in real-time on the web as they came in. This format created an exciting atmosphere, where competitors and others could continously monitor how the contest was proceeding. Twelve submitted solvers competed in some or all of seven competition divisions, with each division corresponding to an SMT-LIB logic. Each division had around 50 problems, drawn from a larger set of 1338 benchmarks which the organizers, with the help of a number of other researchers, had collected and translated into SMT-LIB format. Solvers ran with a time limit of 10 minutes and a memory limit of a little over 512 MB, which was the amount of physical memory on the Linux machines made available by the University of Edinburghsolvers (which parse SMT-LIB format).

SMT-COMP'05 appears to be viewed as having been very successful, due to the creation of so many benchmarks in SMT-LIB format, and the larger than expected number of entered solvers. SMT-COMP'05 provided just the kind of jump start to the SMT-LIB initiative's standardization and benchmark collection activities that it had been proposed to provide.

Last modified: Tue 17 Feb 2015 15:01 UTC