[DL] Announcing SMT-COMP 2006

[Clark Barrett]

Please distribute.  Apologies for multiple postings...

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

                          CAV'06 Satellite Event

       2nd International Satisfiability Modulo Theories Competition
                               (SMT-COMP'06)

                         Seattle, Washington, USA
                            August 16-20, 2006

                            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-COMP aims to spur innovation in
SMT research by providing a yearly friendly competition for SMT solvers.

SMT-COMP came out of discussions surrounding the SMT-LIB initiative, an
initiative of the SMT community to build a library of SMT benchmarks in a
proposed standard format.  SMT-COMP helps 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 SMT-COMP meeting which will take place on the evening of August 20.
For more information, please see the SMT-COMP web page at
http://www.csl.sri.com/users/demoura/smt-comp/

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

The potential benchmark divisions for this year will include all of the
divisions represented last year as well as several new ones.  For detailed
descriptions of the divisions, refer to the SMT-LIB web page at
http://goedel.cs.uiowa.edu/smtlib/

* 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 (Arrays): Quantifier-free formulas over the theory
  of arrays (with 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 extensional
  arrays.

* QF_UFBV[32] (Bit-vectors and Uninterpreted Functions)
  Unquantified formulas over bit vectors of size up to 32 bits, with unintepreted
  function, and predicate symbols.

* 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 extensional
  arrays.

* AUFLIRA: (Arrays, Uninterpreted Functions, and Linear Arithmetic)
  This division consists of formulas with quantifiers, arrays of reals indexed
  by integers (Array1), arrays of Array1 indexed by integers (Array2), and
  linear arithmetic over the integers and reals.  This division is included to
  accommodate a large number of quantified verification benchmarks that have
  become available.

As with last year, we reserve the right to remove benchmark divisions if we do
not receive enough quality benchmarks or enough solvers in a particular
division.  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
---------------

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

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

    * June 1:    First version of the benchmark library posted for comment.
    * July 1:    Revised version of the benchmark library posted. Pseudo-random
                 benchmark selector becomes available.
    * August 1:  Final version of the benchmark library posted, and system
                 submission opened.
    * August 8:  Final system description due, with magic numbers for
                 pseudo-random selection of benchmarks.
    * August 9:  Selected benchmarks posted.
    * August 16: Competition begins, coinciding with the start of CAV.

-----------------
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/

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