×

The 2013 evaluation of SMT-COMP and SMT-LIB. (English) Zbl 1356.68185

Summary: After 8 years of SMT Competitions, the SMT Steering Committee decided, for 2013, to sponsor an evaluation of the status of SMT benchmarks and solvers, rather than another competition. This report summarizes the results of the evaluation, conducted by the authors. The key observations are that (1) the competition results are quite sensitive to randomness and (2) the most significant need for the future is assessment and improvement of benchmarks in the light of SMT applications. The evaluation also measured competitiveness of solvers, general coverage of solvers, logics, and benchmarks, and degree of repeatability of measurements and competitions.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

StarExec; SMT-LIB
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aziz, M.A.: A novel portfolio solver for satisfiability modulo theory problems (2013) · Zbl 1019.68101
[2] Aziz, M.A., Wassal, A., Darwish, N.: A machine learning technique for hardness estimation of QFBV SMT problems (work in progress). In: SMT Workshop 2012 10th International Workshop on Satisfiability Modulo Theories SMT-COMP 2012, p. 56 (2012)
[3] Barrett, C., Deters, M., de Moura, L., Oliveras, A.: A stump. 6 years of SMT-COMP (2012)
[4] Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A, Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England) (2010)
[5] Le Berre, D., Simon, L.: The essentials of the SAT 2003 competition. In: Sixth international conference on theory and applications of satisfiability testing, vol. 2919 of LNCS, pp. 452-467. Springer (2003) · Zbl 1204.68203
[6] Pelletier, F.J., Sutcliffe, G., Suttner, C.B.: The Development of CASC. AI Communications 15(2-3), 79-90 (2002) · Zbl 1019.68101
[7] Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proceedings of the 7th international joint conference on automated reasoning, Lecture Notes in Artificial Intelligence. Springer (2014) · Zbl 06348250
[8] Sutcliffe, G.: The CADE ATP System Competition Design and Organization., http://www.cs.miami.edu/tptp/CASC/24/Design.html#Evaluation · Zbl 1126.68580
[9] Federated logic conference (FLoC) olympic games. http://vsl2014.at/olympics/ · Zbl 1019.68101
[10] The SMT-COMP web site provides results of the SMT competition and links to the system descriptions of the participants., http://smtcomp.org
[11] StarExec web site., http://www.starexec.org
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.