6 Years of SMT-COMP

Clark Barrett, Morgan Deters, Leonardo De Moura, Albert Oliveras, Aaron Stump

Research output: Contribution to journalArticle

Abstract

The annual Satisfiability Modulo Theories Competition (SMT-COMP) was initiated in 2005 in order to stimulate the advance of state-of-the-art techniques and tools developed by the Satisfiability Modulo Theories (SMT) community. This paper summarizes the first six editions of the competition. We present the evolution of the competition's organization and rules, show how the state of the art has improved over the course of the competition, and discuss the impact SMT-COMP has had on the SMT community and beyond. Additionally, we include an exhaustive list of all competitors, and present experimental results showing significant improvement in SMT solvers during these six years. Finally, we analyze to what extent the initial goals of the competition have been achieved, and sketch future directions for the competition.

Original languageEnglish (US)
Pages (from-to)243-277
Number of pages35
JournalJournal of Automated Reasoning
Volume50
Issue number3
DOIs
StatePublished - 2013

Keywords

  • Competition
  • Experimental evaluation
  • SAT Modulo Theories

ASJC Scopus subject areas

  • Artificial Intelligence
  • Software
  • Computational Theory and Mathematics

Cite this

Barrett, C., Deters, M., De Moura, L., Oliveras, A., & Stump, A. (2013). 6 Years of SMT-COMP. Journal of Automated Reasoning, 50(3), 243-277. https://doi.org/10.1007/s10817-012-9246-5

6 Years of SMT-COMP. / Barrett, Clark; Deters, Morgan; De Moura, Leonardo; Oliveras, Albert; Stump, Aaron.

In: Journal of Automated Reasoning, Vol. 50, No. 3, 2013, p. 243-277.

Research output: Contribution to journalArticle

Barrett, C, Deters, M, De Moura, L, Oliveras, A & Stump, A 2013, '6 Years of SMT-COMP', Journal of Automated Reasoning, vol. 50, no. 3, pp. 243-277. https://doi.org/10.1007/s10817-012-9246-5
Barrett C, Deters M, De Moura L, Oliveras A, Stump A. 6 Years of SMT-COMP. Journal of Automated Reasoning. 2013;50(3):243-277. https://doi.org/10.1007/s10817-012-9246-5
Barrett, Clark ; Deters, Morgan ; De Moura, Leonardo ; Oliveras, Albert ; Stump, Aaron. / 6 Years of SMT-COMP. In: Journal of Automated Reasoning. 2013 ; Vol. 50, No. 3. pp. 243-277.
@article{a1d8d027a34247ceb2b6a129ad4c3152,
title = "6 Years of SMT-COMP",
abstract = "The annual Satisfiability Modulo Theories Competition (SMT-COMP) was initiated in 2005 in order to stimulate the advance of state-of-the-art techniques and tools developed by the Satisfiability Modulo Theories (SMT) community. This paper summarizes the first six editions of the competition. We present the evolution of the competition's organization and rules, show how the state of the art has improved over the course of the competition, and discuss the impact SMT-COMP has had on the SMT community and beyond. Additionally, we include an exhaustive list of all competitors, and present experimental results showing significant improvement in SMT solvers during these six years. Finally, we analyze to what extent the initial goals of the competition have been achieved, and sketch future directions for the competition.",
keywords = "Competition, Experimental evaluation, SAT Modulo Theories",
author = "Clark Barrett and Morgan Deters and {De Moura}, Leonardo and Albert Oliveras and Aaron Stump",
year = "2013",
doi = "10.1007/s10817-012-9246-5",
language = "English (US)",
volume = "50",
pages = "243--277",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "3",

}

TY - JOUR

T1 - 6 Years of SMT-COMP

AU - Barrett, Clark

AU - Deters, Morgan

AU - De Moura, Leonardo

AU - Oliveras, Albert

AU - Stump, Aaron

PY - 2013

Y1 - 2013

N2 - The annual Satisfiability Modulo Theories Competition (SMT-COMP) was initiated in 2005 in order to stimulate the advance of state-of-the-art techniques and tools developed by the Satisfiability Modulo Theories (SMT) community. This paper summarizes the first six editions of the competition. We present the evolution of the competition's organization and rules, show how the state of the art has improved over the course of the competition, and discuss the impact SMT-COMP has had on the SMT community and beyond. Additionally, we include an exhaustive list of all competitors, and present experimental results showing significant improvement in SMT solvers during these six years. Finally, we analyze to what extent the initial goals of the competition have been achieved, and sketch future directions for the competition.

AB - The annual Satisfiability Modulo Theories Competition (SMT-COMP) was initiated in 2005 in order to stimulate the advance of state-of-the-art techniques and tools developed by the Satisfiability Modulo Theories (SMT) community. This paper summarizes the first six editions of the competition. We present the evolution of the competition's organization and rules, show how the state of the art has improved over the course of the competition, and discuss the impact SMT-COMP has had on the SMT community and beyond. Additionally, we include an exhaustive list of all competitors, and present experimental results showing significant improvement in SMT solvers during these six years. Finally, we analyze to what extent the initial goals of the competition have been achieved, and sketch future directions for the competition.

KW - Competition

KW - Experimental evaluation

KW - SAT Modulo Theories

UR - http://www.scopus.com/inward/record.url?scp=84878563375&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84878563375&partnerID=8YFLogxK

U2 - 10.1007/s10817-012-9246-5

DO - 10.1007/s10817-012-9246-5

M3 - Article

VL - 50

SP - 243

EP - 277

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 3

ER -