Hardware model checking competition 2014: An analysis and comparison of solvers and benchmarks

Tutkimustuotos: Lehtiartikkelivertaisarvioitu

Standard

Hardware model checking competition 2014: An analysis and comparison of solvers and benchmarks. / Cabodi, Gianpiero; Loiacono, Carmelo; Palena, Marco; Pasini, Paolo; Patti, Denis; Quer, Stefano; Vendraminetto, Danilo; Biere, Armin; Heljanko, Keijo.

julkaisussa: Journal of Satisfiability, Boolean Modeling and Computation, Vuosikerta 9, 28.01.2016, s. 135-172.

Tutkimustuotos: Lehtiartikkelivertaisarvioitu

Harvard

Cabodi, G, Loiacono, C, Palena, M, Pasini, P, Patti, D, Quer, S, Vendraminetto, D, Biere, A & Heljanko, K 2016, 'Hardware model checking competition 2014: An analysis and comparison of solvers and benchmarks', Journal of Satisfiability, Boolean Modeling and Computation, Vuosikerta. 9, Sivut 135-172.

APA

Vancouver

Author

Cabodi, Gianpiero ; Loiacono, Carmelo ; Palena, Marco ; Pasini, Paolo ; Patti, Denis ; Quer, Stefano ; Vendraminetto, Danilo ; Biere, Armin ; Heljanko, Keijo. / Hardware model checking competition 2014: An analysis and comparison of solvers and benchmarks. Julkaisussa: Journal of Satisfiability, Boolean Modeling and Computation. 2016 ; Vuosikerta 9. Sivut 135-172.

Bibtex - Lataa

@article{5872bf46b7dc47f6a39e9d4e26a4959c,
title = "Hardware model checking competition 2014: An analysis and comparison of solvers and benchmarks",
abstract = "Model checkers and sequential equivalence checkers have become essential tools for the semiconductor industry in recent years. The Hardware Model Checking Competition (HWMCC) was founded in 2006 with the purpose of intensifying research interest in these technologies, and establishing more of a science behind them. For example, the competition provided a standardized benchmark format, a challenging and diverse set of industrially- relevant public benchmarks, and, as a consequence, a significant motivation for additional research to advance the state-of-the-art in model checkers for these verification problems. This paper provides a historical perspective, and an analysis of the tools and benchmarks submitted to the competition. It also presents a detailed analysis of the results collected in the 2014 edition of the contest, showing relations among tools, and among tools and benchmarks. It finally proposes a list of considerations, lessons learned, and hints for both future organizers and competitors.",
keywords = "model checking, equivalence checking, binary decisions diagrams, satisfiability solvers, interpolation, IC3, property directed reachability",
author = "Gianpiero Cabodi and Carmelo Loiacono and Marco Palena and Paolo Pasini and Denis Patti and Stefano Quer and Danilo Vendraminetto and Armin Biere and Keijo Heljanko",
year = "2016",
month = "1",
day = "28",
language = "English",
volume = "9",
pages = "135--172",
journal = "Journal of Satisfiability, Boolean Modeling and Computation",
issn = "1875-5011",
publisher = "IOS PRESS",

}

RIS - Lataa

TY - JOUR

T1 - Hardware model checking competition 2014: An analysis and comparison of solvers and benchmarks

AU - Cabodi, Gianpiero

AU - Loiacono, Carmelo

AU - Palena, Marco

AU - Pasini, Paolo

AU - Patti, Denis

AU - Quer, Stefano

AU - Vendraminetto, Danilo

AU - Biere, Armin

AU - Heljanko, Keijo

PY - 2016/1/28

Y1 - 2016/1/28

N2 - Model checkers and sequential equivalence checkers have become essential tools for the semiconductor industry in recent years. The Hardware Model Checking Competition (HWMCC) was founded in 2006 with the purpose of intensifying research interest in these technologies, and establishing more of a science behind them. For example, the competition provided a standardized benchmark format, a challenging and diverse set of industrially- relevant public benchmarks, and, as a consequence, a significant motivation for additional research to advance the state-of-the-art in model checkers for these verification problems. This paper provides a historical perspective, and an analysis of the tools and benchmarks submitted to the competition. It also presents a detailed analysis of the results collected in the 2014 edition of the contest, showing relations among tools, and among tools and benchmarks. It finally proposes a list of considerations, lessons learned, and hints for both future organizers and competitors.

AB - Model checkers and sequential equivalence checkers have become essential tools for the semiconductor industry in recent years. The Hardware Model Checking Competition (HWMCC) was founded in 2006 with the purpose of intensifying research interest in these technologies, and establishing more of a science behind them. For example, the competition provided a standardized benchmark format, a challenging and diverse set of industrially- relevant public benchmarks, and, as a consequence, a significant motivation for additional research to advance the state-of-the-art in model checkers for these verification problems. This paper provides a historical perspective, and an analysis of the tools and benchmarks submitted to the competition. It also presents a detailed analysis of the results collected in the 2014 edition of the contest, showing relations among tools, and among tools and benchmarks. It finally proposes a list of considerations, lessons learned, and hints for both future organizers and competitors.

KW - model checking

KW - equivalence checking

KW - binary decisions diagrams

KW - satisfiability solvers

KW - interpolation

KW - IC3

KW - property directed reachability

M3 - Article

VL - 9

SP - 135

EP - 172

JO - Journal of Satisfiability, Boolean Modeling and Computation

JF - Journal of Satisfiability, Boolean Modeling and Computation

SN - 1875-5011

ER -

ID: 10327672