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