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

Clark Barrett, Leonardo De Moura, Aaron Stump

Research output: Contribution to journalArticle

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 languageEnglish (US)
Pages (from-to)373-390
Number of pages18
JournalJournal of Automated Reasoning
Volume35
Issue number4
DOIs
StatePublished - Nov 2005

Fingerprint

Surface mount technology
Electric sparks
Hardware

Keywords

  • Competition
  • Decision procedures
  • Satisfiability modulo theories

ASJC Scopus subject areas

  • Artificial Intelligence

Cite this

Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). / Barrett, Clark; De Moura, Leonardo; Stump, Aaron.

In: Journal of Automated Reasoning, Vol. 35, No. 4, 11.2005, p. 373-390.

Research output: Contribution to journalArticle

Barrett, Clark ; De Moura, Leonardo ; Stump, Aaron. / Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). In: Journal of Automated Reasoning. 2005 ; Vol. 35, No. 4. pp. 373-390.
@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 = "11",
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 -