[FOM] Announcing SMT-COMP 2009

[Clark Barrett]

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

                           CADE-22 Satellite Event

        5th International Satisfiability Modulo Theories Competition
                                (SMT-COMP'09)

                               Montreal, Canada
                                  August 2009

                             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.

As part of SMT-COMP, a special session will be held at SMT Workshop in
which the competitors will have a chance to present their tools and
discuss them with other competitors. More information about the SMT
Workshop can be found on the web page: http://ie.technion.ac.il/SMT09

The highlights of SMT-COMP 2009 are covered below.  For the latest
information, please see the SMT-COMP web page at:

http://www.smtcomp.org/

------------------------------------------
Main changes with respect to SMT-COMP 2008
------------------------------------------

- Use of 64-bit architecture in the SMT-Exec service for solver execution.

- Small updates to the benchmark selection algorithms.

- Elimination of the disqualification rule for solvers giving four or more
   wrong answers in a division; rather, the scoring system alone will
   punish solvers that give incorrect answers.

For more detailed information please refer to the rules posted at
http://www.smtcomp.org/.

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

The potential benchmark divisions for this year include all of the
divisions represented last year. We do not anticipate new divisions
this year unless quality benchmarks are collected. For detailed
descriptions of the divisions, refer to the SMT-LIB web page at
http://www.smtlib.org/

* QF_UF (Uninterpreted Functions): 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): 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): 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 is similar to QF_LRA, except that it also allows
   uninterpreted functions and predicates.

* QF_AX (Arrays with Extensionality): quantifier-free formulas to be
   tested for satisfiability modulo a background theory of arrays which
   includes the extensionality axiom.

* QF_AUFLIA (Linear Integer Arithmetic with Uninterpreted Functions
   and Arrays): 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_BV (Fixed-size Bit-vectors): quantifier-free formulas over bit
   vectors of fixed size.

* QF_AUFBV (Bit-vectors with Arrays and Uninterpreted Functions):
   quantifier-free formulas over bit vectors of fixed size, with arrays
   and uninterpreted functions and predicate symbols.

* AUFLIA+p (Linear Integer Arithmetic with Uninterpreted Functions and
   Arrays): quantified formulas to be tested for satisfiability modulo
   a background theory combining linear integer arithmetic,
   uninterpreted function and predicate symbols, and extensional
   arrays. Benchmarks include patterns for guiding instantiation
   mechanisms.

* AUFLIA-p (Linear Integer Arithmetic with Uninterpreted Functions and
   Arrays): formulas from AUFLIA+p once all patterns have been
   removed.

* AUFLIRA (Arrays, Uninterpreted Functions, and Linear Arithmetic):
   quantifier formulas with arrays of reals indexed by integers
   (Array1), arrays of Array1 indexed by integers (Array2), and linear
   arithmetic over the integers and reals.

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

Solvers will be submitted via the SMT-Exec service (http://www.smtexec.org/)
this year, as in 2008.  Please refer to http://www.smtcomp.org/ for
complete details on entering the competition.

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

  * June 1:     First version of SMT-COMP 2009 benchmarks posted for
                comment.

  * July 1:     No new benchmarks can be added after this date, but
                problems with existing benchmarks may be fixed.

  * July 24:    Benchmark library is frozen.

  * July 30:    Final version of solvers due via SMT-Exec, with magic
    (7pm ET)    numbers for pseudo-random selection of benchmarks.

  * August 1:   Close of two-day grace period for resubmission of
    (7pm ET)    entries.

  * August 2-3: SMT Workshop.

  * August 4-7: Anticipated dates for competition.

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

Clark Barrett   (New York University, barrett at cs.nyu.edu)
Morgan Deters   (Technical Univ. of Catalonia, mdeters at lsi.upc.edu)
Albert Oliveras (Technical Univ. of Catalonia, oliveras at lsi.upc.edu)
Aaron Stump     (The University of Iowa, astump at cs.uiowa.edu )

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

For details on the competition, see
http://www.smtcomp.org/

For more information on the SMT-LIB format, see
http://www.smtlib.org/

For more information about the SMT Workshop, see
http://ie.technion.ac.il/SMT09

SMT-COMP is partially sponsored by the U.S. National Science Foundation,
under grant CNS-0551697.