[TYPES] Announcing SMT-COMP

[Clark Barrett]

Please distribute.  Apologies for multiple postings...

===========================================================================

                          CAV'05 Satellite Event

       1st International Satisfiability Modulo Theories Competition
                               (SMT-COMP'05)

                          Edinburgh, Scotland, UK
                              July 6-10, 2005

                            CALL FOR BENCHMARKS
                             CALL FOR ENTRANTS

===========================================================================

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.

---------------
Benchmarks
---------------

The first SMT-COMP will feature benchmarks in the following problem divisions
(these divisions correspond to SMT-LIB logics: see
http://goedel.cs.uiowa.edu/smtlib/ for more details).

* QF_UF (Uninterpreted Functions): This division consists of quantifier-free
  formulas whose satisfiability is to be decided modulo the empty theory. Each
  benchmark may introduce its own uninterpreted function and predicate symbols.

* QF_IDL (Integer Difference Logic): This division consists of quantifier-free
  formulas to be tested for satisfiability modulo a background theory of
  integer arithmetic.  The syntax of atomic formulas is restricted to
  difference logic, i.e. x - y op c, where op is either equality or inequality
  and c is an integer constant.

* QF_RDL (Real Difference Logic): This division is like QF_IDL, except that the
  background theory is real arithmetic.

* QF_UFIDL (Integer Difference Logic with Uninterpreted Functions): This
  division contains benchmarks in a logic which is similar to QF_IDL, except
  that it also allows uninterpreted functions and predicates.

* QF_LIA (Linear Integer Arithmetic): This division consists of quantifier-free
  formulas to be tested for satisfiability modulo a background theory of
  integer arithmetic.  The syntax of atomic formulas is restricted to contain
  only linear terms.

* QF_LRA (Linear Real Arithmetic): This division is like QF_LIA, except that
  the background theory is real arithmetic.

* QF_UFLIA (Linear Integer Arithmetic with Uninterpreted Functions): This
  division contains benchmarks in a logic which is similar to QF_LIA, except
  that it also allows uninterpreted functions and predicates.

* QF_UFLRA (Linear Real Arithmetic with Uninterpreted Functions): This division
  contains benchmarks in a logic which is similar to QF_LRA, except that it
  also allows uninterpreted functions and predicates.

* QF_A (Non-extensional Arrays): Quantifier-free formulas over the theory
  of arrays without extensionality.

* QF_AUFLIA (Linear Integer Arithmetic with Uninterpreted Functions and
  Arrays): This division consists of quantifier-free formulas to be tested for
  satisfiability modulo a background theory combining linear integer
  arithmetic, uninterpreted function and predicate symbols, and non-extensional
  arrays.

* AUFLIA: (Linear Integer Arithmetic with Uninterpreted Functions and Arrays)
  This division consists of formulas with quantifiers to be tested for
  satisfiability modulo a background theory combining linear integer
  arithmetic, uninterpreted function and predicate symbols, and non-extensional
  arrays.

We have collected an initial set of benchmarks in the SMT-LIB format, but we
are looking for additional benchmarks in all divisions, (especially in QF_UF,
QF_IDL, QF_A, and AUFLIA).  If you have access to benchmarks in any of these
divisions, even if they are not in the SMT-LIB format, please contact one of
the organizers (see below).

---------------
Solvers
---------------

System pre-registration and submission is now open.

Please refer to http://www.csl.sri.com/users/demoura/smt-comp/index.shtml for
complete details on entering the competition.

---------------
Important Dates
---------------

Intent to Register: May 15, 2005
System Submission: June 20, 2005
Competition: July 6-10, 2005

-----------------
Organizers
-----------------

Clark Barrett (New York University, barrett at cs.nyu.edu)
Leonardo de Moura (SRI International, demoura at csl.sri.com)
Aaron Stump (Washington University in St. Louis, stump at cse.wustl.edu)

----------------
More Information
----------------

For details on the competition, see
http://www.csl.sri.com/users/demoura/smt-comp/index.shtml

For more information on the smt-lib format, see
http://goedel.cs.uiowa.edu/smtlib/