Wednesday
Thursday
Friday
Saturday
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.
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.
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.
The methodology and the results of the competition will be presented at the end of CAV, and a more detailed discussion of the competition will take place in a special session of the PDPAR workshop following CAV.