The 2013 Evaluation of SMT-COMP and SMT-LIB

David Cok; Aaron Stump; Tjark Weber

doi:10.1007/s10817-015-9328-2

Back

The 2013 Evaluation of SMT-COMP and SMT-LIB

Journal article

Peer reviewed

The 2013 Evaluation of SMT-COMP and SMT-LIB

David Cok, Aaron Stump and Tjark Weber

Journal of automated reasoning, Vol.55(1), pp.61-90

06/2015

DOI: 10.1007/s10817-015-9328-2

View Online

Abstract

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.

SMT-COMP

Competition

Computer Science

Artificial Intelligence (incl. Robotics)

Model checking

Symbolic and Algebraic Manipulation

SMT solvers

SMT-LIB

Mathematical Logic and Foundations

Mathematical Logic and Formal Languages

Details

Title: Subtitle: The 2013 Evaluation of SMT-COMP and SMT-LIB
Creators: David Cok - GrammaTech, Inc. Ithaca NY USA
Aaron Stump - University of Iowa Iowa City IA USA
Tjark Weber - Uppsala University Uppsala Sweden
Resource Type: Journal article
Publication Details: Journal of automated reasoning, Vol.55(1), pp.61-90
DOI: 10.1007/s10817-015-9328-2
ISSN: 0168-7433
eISSN: 1573-0670
Publisher: Springer Netherlands; Dordrecht
Language: English
Date published: 06/2015
Academic Unit: Computer Science
Record Identifier: 9984002498402771

Metrics

14 Record Views

9 Times Cited - Web of Science