Logic List Mailing Archive
Call for Benchmarks for the 2nd SMT-COMP (Seattle WA), Aug 2006
2nd International Satisfiability Modulo Theories Competition
(SMT-COMP'06)
[CAV'06 Satellite Event]
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@cs.nyu.edu)
Leonardo de Moura (SRI International, demoura@csl.sri.com)
Aaron Stump (Washington University in St. Louis, stump@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/