Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)

Clark Barrett; Leonardo De Moura; Aaron Stump

doi:10.1007/s10817-006-9026-1

Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)

Clark Barrett, Leonardo De Moura, Aaron Stump

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

The Satisfiability Modulo Theories Competition (SMT-COMP) is intended to spark further advances in the decision procedures field, especially for applications in hardware and software verification. Public competitions are a well-known means of stimulating advancement in automated reasoning. Evaluation of SMT solvers entered in SMT-COMP took place while CAV 2005 was meeting. Twelve solvers were entered; 1,352 benchmarks were collected in seven different divisions.

Original language	English (US)
Pages (from-to)	373-390
Number of pages	18
Journal	Journal of Automated Reasoning
Volume	35
Issue number	4
DOIs	https://doi.org/10.1007/s10817-006-9026-1
State	Published - Nov 2005

Keywords

Competition
Decision procedures
Satisfiability modulo theories

ASJC Scopus subject areas

Software
Computational Theory and Mathematics
Artificial Intelligence

Access to Document

10.1007/s10817-006-9026-1

Fingerprint Dive into the research topics of 'Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)'. Together they form a unique fingerprint.

Cite this

@article{058b690026034ad09ca192616ae8842b,

title = "Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)",

abstract = "The Satisfiability Modulo Theories Competition (SMT-COMP) is intended to spark further advances in the decision procedures field, especially for applications in hardware and software verification. Public competitions are a well-known means of stimulating advancement in automated reasoning. Evaluation of SMT solvers entered in SMT-COMP took place while CAV 2005 was meeting. Twelve solvers were entered; 1,352 benchmarks were collected in seven different divisions.",

keywords = "Competition, Decision procedures, Satisfiability modulo theories",

author = "Clark Barrett and {De Moura}, Leonardo and Aaron Stump",

year = "2005",

month = nov,

doi = "10.1007/s10817-006-9026-1",

language = "English (US)",

volume = "35",

pages = "373--390",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "4",

}

TY - JOUR

T1 - Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)

AU - Barrett, Clark

AU - De Moura, Leonardo

AU - Stump, Aaron

PY - 2005/11

Y1 - 2005/11

N2 - The Satisfiability Modulo Theories Competition (SMT-COMP) is intended to spark further advances in the decision procedures field, especially for applications in hardware and software verification. Public competitions are a well-known means of stimulating advancement in automated reasoning. Evaluation of SMT solvers entered in SMT-COMP took place while CAV 2005 was meeting. Twelve solvers were entered; 1,352 benchmarks were collected in seven different divisions.

AB - The Satisfiability Modulo Theories Competition (SMT-COMP) is intended to spark further advances in the decision procedures field, especially for applications in hardware and software verification. Public competitions are a well-known means of stimulating advancement in automated reasoning. Evaluation of SMT solvers entered in SMT-COMP took place while CAV 2005 was meeting. Twelve solvers were entered; 1,352 benchmarks were collected in seven different divisions.

KW - Competition

KW - Decision procedures

KW - Satisfiability modulo theories

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

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

U2 - 10.1007/s10817-006-9026-1

DO - 10.1007/s10817-006-9026-1

M3 - Article

AN - SCOPUS:33750192589

VL - 35

SP - 373

EP - 390

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 4

ER -