Introducing Certificates to the Hardware Model Checking Competition

Nils Froleyks; Emily Yu; Mathias Preiner; Armin Biere; Keijo Heljanko

doi:10.1007/978-3-031-98668-0_14

Introducing Certificates to the Hardware Model Checking Competition

Nils Froleyks^*
, Emily Yu
, Mathias Preiner
, Armin Biere
, Keijo Heljanko

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.

Original language	English
Title of host publication	Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings
Subtitle of host publication	37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I
Editors	Ruzica Piskac, Zvonimir Rakamarić
Publisher	Springer, Cham
Pages	281-295
Number of pages	15
Edition	1
ISBN (Electronic)	978-3-031-98668-0
ISBN (Print)	978-3-031-98667-3
DOIs	https://doi.org/10.1007/978-3-031-98668-0_14
Publication status	Published - Jul 2025

Publication series

Name	Lecture Notes in Computer Science
Volume	15931 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Fields of science

102031 Theoretical computer science
603109 Logic
102011 Formal languages
102022 Software development
102001 Artificial intelligence
202006 Computer hardware
102 Computer Sciences
101019 Stochastics
102003 Image processing
103029 Statistical physics
101018 Statistics
101017 Game theory
202017 Embedded systems
101016 Optimisation
101015 Operations research
101014 Numerical mathematics
101029 Mathematical statistics
101028 Mathematical modelling
101026 Time series analysis
101024 Probability theory
102032 Computational intelligence
102004 Bioinformatics
102013 Human-computer interaction
101027 Dynamical systems
305907 Medical statistics
101004 Biomathematics
305905 Medical informatics
101031 Approximation theory
102033 Data mining
305901 Computer-aided diagnosis and therapy
102019 Machine learning
106007 Biostatistics
102018 Artificial neural networks
106005 Bioinformatics
202037 Signal processing
202036 Sensor systems
202035 Robotics

JKU Focus areas

Digital Transformation

Access to Document

10.1007/978-3-031-98668-0_14Licence: CC BY

Cite this

Froleyks, N., Yu, E., Preiner, M., Biere, A., & Heljanko, K. (2025). Introducing Certificates to the Hardware Model Checking Competition. In R. Piskac, & Z. Rakamarić (Eds.), Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings: 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I (1 ed., pp. 281-295). (Lecture Notes in Computer Science; Vol. 15931 LNCS). Springer, Cham. https://doi.org/10.1007/978-3-031-98668-0_14

Froleyks, Nils ; Yu, Emily ; Preiner, Mathias et al. / Introducing Certificates to the Hardware Model Checking Competition. Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings: 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I. editor / Ruzica Piskac ; Zvonimir Rakamarić. 1. ed. Springer, Cham, 2025. pp. 281-295 (Lecture Notes in Computer Science).

@inproceedings{69f7c43246194839bdd81228cfef690a,

title = "Introducing Certificates to the Hardware Model Checking Competition",

abstract = "Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.",

author = "Nils Froleyks and Emily Yu and Mathias Preiner and Armin Biere and Keijo Heljanko",

year = "2025",

month = jul,

doi = "10.1007/978-3-031-98668-0\_14",

language = "English",

isbn = "978-3-031-98667-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Cham",

pages = "281--295",

editor = "Ruzica Piskac and Zvonimir Rakamari{\'c}",

booktitle = "Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings",

edition = "1",

}

Froleyks, N, Yu, E, Preiner, M, Biere, A & Heljanko, K 2025, Introducing Certificates to the Hardware Model Checking Competition. in R Piskac & Z Rakamarić (eds), Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings: 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I. 1 edn, Lecture Notes in Computer Science, vol. 15931 LNCS, Springer, Cham, pp. 281-295. https://doi.org/10.1007/978-3-031-98668-0_14

Introducing Certificates to the Hardware Model Checking Competition. / Froleyks, Nils; Yu, Emily; Preiner, Mathias et al.
Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings: 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I. ed. / Ruzica Piskac; Zvonimir Rakamarić. 1. ed. Springer, Cham, 2025. p. 281-295 (Lecture Notes in Computer Science; Vol. 15931 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - Introducing Certificates to the Hardware Model Checking Competition

AU - Froleyks, Nils

AU - Yu, Emily

AU - Preiner, Mathias

AU - Biere, Armin

AU - Heljanko, Keijo

PY - 2025/7

Y1 - 2025/7

N2 - Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.

AB - Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.

UR - https://www.scopus.com/pages/publications/105012423702

U2 - 10.1007/978-3-031-98668-0_14

DO - 10.1007/978-3-031-98668-0_14

M3 - Conference proceedings

SN - 978-3-031-98667-3

T3 - Lecture Notes in Computer Science

SP - 281

EP - 295

BT - Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings

A2 - Piskac, Ruzica

A2 - Rakamarić, Zvonimir

PB - Springer, Cham

ER -

Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing Certificates to the Hardware Model Checking Competition. In Piskac R, Rakamarić Z, editors, Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings: 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I. 1 ed. Springer, Cham. 2025. p. 281-295. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-98668-0_14

Introducing Certificates to the Hardware Model Checking Competition

Abstract

Publication series

Fields of science

JKU Focus areas

Access to Document

Other files and links