[SMT-LIB] New SMT-LIB release for SMT-COMP 2011 -- (multi-query) application track benchmakrs

[Roberto Bruttomesso]

Dear All,

as a follow-up of the previous message about (standard single query)
benchmarks additions.

Here is the frozen set of (multi query) benchmarks for the new
application track of SMT-COMP'11

- QF_UFLIA benchmarks, from Blast

 These are just logs of the calls to the Simplify theorem prover, used
 by Blast when trying to model check some C programs (the name of the
 program is reflected in the name of the benchmark -- original Simplify traces
 can be made available for those who are interested)

- QF_LRA BMC and k-Induction problems on networks of hybrid automata, from NuSMV

 These are benchmarks for hybrid automata, generated by unrolling the
NuSMV models and checking
 them with BMC or k-Induction

- QF_BV and QF_LIA BMC and k-Induction problems on SystemC designs, from NuSMV

 These two are unrollings of translation of some SystemC programs into
 NuSMV. The programs were those used, e.g., in the FMCAD'10 paper:
 "Verifying SystemC: a Software Model Checking Approach" by
 Alessandro Cimatti, Andrea Micheli, Iman Narasamdya and Marco Roveri
 The two sets are essentially the same, except for the different logic
 used.

- QF_LIA BMC and k-Induction problems on Lustre programs, from NuSMV

 These are were obtained from subset of the Lustre models also used for
 the KIND set, except that they were generated from a NuSMV version of
 the Lustre programs, by NuSMV itself.

- QF_UFIDL k-induction problems (postprocessed for competition)

 These benchmarks were obtained from the KIND tool during Lustre
programs verification

- UFLRA benchmarks obtained from ASASP tool, (postprocessed for competition).

 ASASP (http://st.fbk.eu/ASASP) implements a symbolic reachability
procedure for the analysis
 of administrative access control policies. A more detailed
description of the benchmarks can be found in the following paper:
 Analysis of  Administrative Attribute-based RBAC-Policies, by F.
Alberti, A. Armando, and S. Ranise. Efficient Symbolic Automated
 http://st.fbk.eu/sites/st.fbk.eu/files/asiaccs174-alberti.pdf



The benchmarks are available from

http://www.smtcomp.org/2011/application.shtml

The statuses for the queries contained in these benchmarks has not
been determined yet for most of them. Those which are know at this
time will be made available from the same page above in the next few hours.

We will provide the missing statuses as soon as they will be available
to us. Recall that benchmarks with unknown status as of June 15th will
not be considered for the competition.

Since the benchmarks contain multiple (check-sat) commands, each
benchmark FILENAME.smt2 is associated
with a set of answers listed in a file FILENAME.results.txt (those
marked with "untrusted" have been determined with just one solver).
Clearly, the first (check-sat) command is associated with the first
answer in the file, the second (check-sat) with the second answer, and
so on. This format is parsed by the trace executor already available.




The SMTCOMP'11 Organizers
Roberto, Morgan, and Alberto