[SMT-COMP] Call for BENCHMARKS and SOLVERS for SMT-COMP 2012
Morgan Deters
mdeters at cs.nyu.edu
Thu Apr 12 16:00:18 EDT 2012
---------- Forwarded message ----------
From: David Cok <dcok at grammatech.com>
To: cok at frontiernet.net
Cc: smt-comp at cs.nyu.edu, smt-lib <smt-lib at cs.nyu.edu>
Date: Wed, 11 Apr 2012 22:59:16 -0400
Subject: Re: Call for BENCHMARKS and SOLVERS for SMT-COMP 2012
Planning for this year's SMTCOMP is moving along. This note is a quick
reminder that new benchmarks are very welcome and should be submitted
by this weekend. Let me know if you have something in preparation that
you would like us to include but won't be ready for several days.
- David Cok
On 1/23/2012 5:22 PM, cok at frontiernet.net wrote:
>
> ======================================================================
>
> 8th International Satisfiability Modulo Theories Competition
> (SMT-COMP'12)
>
> June 30 - July 1, 2012
> Manchester, UK
>
> 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 relevant
> benchmarks, and encourage adoption of the SMT-LIB standard, through
> friendly competition. Highlights of SMT-COMP 2012 are covered below.
> The competition has been highly successful and is now in its 8th year.
> For the latest information, please see the SMT-COMP web page at:
>
> http://www.smtcomp.org/
>
> The organizers of the competition and the SMT workshop strongly request
> and encourage the submission of new benchmarks and new or improved solvers.
>
> The event has several tracks: a main track, a parallel track, an
> application track, an unsat-core track, and a proof-generation track.
> Within a track there are one or more divisions, where each division
> uses benchmarks from a specific SMT-LIB logic (or group of logics).
> Some tracks-divisions are competitive, in that the results will be scored
> and winners announced; others are exhibition, meaning that the solvers
> will be evaluated and the results publicized, but no winners will be awarded.
>
> ------------------------------------------
> Main changes with respect to SMT-COMP 2011
> ------------------------------------------
>
> - We are concentrating on just a few of the benchmark divisions this
> year for the main competition. Some divisions, such as QF_UF, are
> subsumed into more expressive logics; others have received only
> light interest. Our goal is to focus the competition on divisions
> of particular interest to applications. All non-competition divisions
> will be run in exhibition mode, if solvers are submitted against them,
> and the results will be displayed and publicly reported.
> As always, we encourage entrants from new research groups.
>
> - We are retaining and accenting last year's "application track" and
> encourage submission of benchmarks and competition against these
> benchmarks.
>
> - The penalty for producing an incorrect result is increased. Competitors
> producing all correct results are ranked above those producing
> incorrect results (a "soft" disqualification for unsound tools).
>
> - We are adding an "unsat core" track.
>
> - We will have an exhibition track of solvers that produce proofs.
>
> - The competition will be run with a new StarExec service, replacing
> the previous SMT-Exec service. At this writing, the new service is
> still being completed and tested; it will be announced later. (The
> previous service will be maintained in reserve.)
>
> For more detailed information please refer to the rules posted at
> http://www.smtcomp.org/.
>
> In order to deliver high-quality benchmarks and to allow participants
> to test their solvers we consider the deadline of April 15 strict.
> Benchmarks arriving thereafter will be included in the library but
> not used for SMT-COMP 2012.
>
> --------------------------------------
> Benchmarks for Main and Parallel Track
> --------------------------------------
>
> New benchmarks in all categories are welcome, particularly those
> representative of applications and those relevant to this year's competition.
>
> The potential main competition benchmark divisions for this year include the
> following divisions. For detailed descriptions of the divisions, refer to the
> SMT-LIB web page at http://www.smtlib.org/
>
> * QF_BV
> * QF_AUFBV
> * QF_UFLIA, including benchmarks from QF_LIA
> * QF_UFLRA, including benchmarks from QF_LRA
> * QF_IDL
> * AUFLIA+p
> * AUFLIA-p
> * AUFNIRA
>
> where the benchmark categories are described below
>
> * 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.
>
> * 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_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.
>
> * 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. ***
>
> We will execute the competition for any benchmark divisions for
> which we have adequate benchmarks and entrants. This is expected to
> include at least the divisions used in 2011: QF_BV, QF_LIA, QF_UFLIA,
> and QF_LRA.
>
> --------------------------------
> Benchmarks for the unsat-core and proof-generation tracks
> --------------------------------
>
> We will develop initial benchmarks for these tracks from existing
> benchmarks. However, we highly encourage submission of benchmarks
> that elucidate particular problems or challenges in determining
> unsatisfiable cores or generating proofs.
>
> Note that, in SMT-LIB format, an unsat-core benchmark must have
> its asserted formulae named (see the standard or contact the organizers).
>
> The organizers are considering and accepting comment on which divisions
> to use for these tracks; those divisions will be announced later.
>
> -------
> Solvers
> -------
>
> Solvers will be submitted via the StarExec service, which will be
> announced later. Please refer to http://www.smtcomp.org/
> for complete details on entering the competition.
>
> ---------------
> Important Dates
> ---------------
>
> * March 15 First version of the benchmark library for the
> application track posted for comment. First version of
> the benchmark scrambler, benchmark selector and trace
> executor made available.
>
> * April 15 Final version of the benchmark scrambler, benchmark
> selector and trace exector made available.
>
> * April 15 No new benchmarks can be added after this date, but
> problems with existing benchmarks may be fixed.
>
> * June 1 Benchmark libraries are frozen.
>
> * June 15 (7pm EDT) Solvers due via StarExec (for all tracks), including
> system descriptions and magic numbers for benchmark
> scrambling.
>
> * June 18 (7pm EDT) Final versions due, fixing any last-minute bugs (this
> marks the end of the weekend grace period for
> submissions).
>
> * June 20 Opening value of NYSE Composite Index used to complete
> random seed.
>
> * June 26 - June 29 Dates of IJCAR main conference
> * June 30 - July 1 Dates of IJCAR workshops, including the SMT workshop.
>
> ----------
> Organizers
> ----------
>
> Roberto Bruttomesso (University of Milan, roberto.bruttomesso at unimi.it)
> David Cok - chief organizer (GrammaTech, Inc., cok at frontiernet.net)
> 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://smt2012.loria.fr/
>
More information about the SMT-COMP
mailing list