[SMT-LIB] Call for benchmarks and entrants: SMT-COMP 2011

[Morgan Deters]

My co-organizers Roberto Bruttomesso and Alberto Griggio and I would
like to announce SMT-COMP 2011, to run during CAV this July in Snowbird.
Details follow, and the rules for this year's edition have been posted
on the website, www.smtcomp.org.

Please distribute this call to interested parties; apologies for multiple
copies.

Thank you,
Morgan Deters
Courant Institute of Mathematical Sciences
New York University


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

    7th International Satisfiability Modulo Theories Competition
                            (SMT-COMP'11)

                          July 14 - 20, 2011
                            Snowbird, Utah

                          CALL FOR BENCHMARKS
                           CALL FOR ENTRANTS

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

SMT-COMP is the annual competition for Satisfiability Modulo Theories
(SMT). The goals of SMT-COMP are to spur solver advances, collect of
benchmarks, and encourage adoption of the SMT-LIB standard, through
friendly competition. Highlights of SMT-COMP 2011 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 2010
------------------------------------------

- introduction of an "application track", based on (simulated)
  incremental model-checking queries, to promote the integration of
  SMT solvers within actual verification frameworks;

- divisions without two competitors will not be run as part of the
  competition; however, divisions may be combined more aggressively
  than in years past to ensure competitiveness.  This will largely
  depend on the final submissions, and will be done with the input
  of the community.

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

--------------------------------------
Benchmarks for Main and Parallel Track
--------------------------------------

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_NIA (Nonlinear Integer Arithmetic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  There is no restriction to linear terms.

* 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, with patterns): 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, without patterns): 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.

* UFNIA+p (Uninterpreted Functions and Nonlinear Arithmetic, patterns
  included): quantifier formulas with uninterpreted functions and
  nonlinear integer arithmetic.

* AUFNIRA (Arrays, Uninterpreted Functions, and Nonlinear Arithmetic):
  quantifier formulas with arrays of reals indexed by integers
  (Array1), arrays of Array1 indexed by integers (Array2), and
  nonlinear 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).

--------------------------------
Benchmarks for Application Track
--------------------------------

Benchmarks for this track exploit the incremental capabilities of
the SMT-LIB2 format, by means of which it is possible to query
the solver multiple times by adding and retracting assertions.
Each benchmark can be thought of as a "trace" dumped from the
interaction of the solver with, e.g., a model-checker. The
benchmarks will be executed using a "trace executor" which
simulates (and abstracts away) the online interaction with the
model checker.

Please refer to the rules for more details.

*** We strongly encourage submissions of benchmarks for this track. ***

In order to deliver high-quality benchmarks and to allow participants
to test their solvers we consider the deadline of May 15 strict.
Benchmarks arriving thereafter will be included in the library but
not used for SMT-COMP 2011.

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

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

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

* March 31          First version of the benchmark library for the
                    application track posted for comment. First version of
                    the benchmark scrambler, benchmark selector and trace
                    exector made available.

* April 30          Final version of the benchmark scrambler, benchmark
                    selector and trace exector made available.

* May 15            No new benchmarks can be added after this date, but
                    problems with existing benchmarks may be fixed.

* June 15           Benchmark libraries are frozen.

* July 9 (7pm ET)   Solvers due via SMT-Exec (for all tracks), including
                    system descriptions and magic numbers for benchmark
                    scrambling.

* July 11 (7pm ET)  Final versions due, fixing any last-minute bugs (this
                    marks the end of the two day grace period for
                    submissions).

* July 12           Opening value of NYSE Composite Index used to complete
                    random seed.

* July 14-20        Anticipated dates for SMT-COMP 2011.

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

Roberto Bruttomesso (University of Lugano, roberto.bruttomesso at usi.ch)
Morgan  Deters      (New York University, mdeters at cs.nyu.edu)
Alberto Griggio     (FBK, griggio at fbk.eu)

----------------
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://uclid.eecs.berkeley.edu/smt11