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

^*Korrespondierende/r Autor/-in für diese Arbeit

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

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.

Originalsprache	Englisch
Titel	Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings
Untertitel	37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I
Herausgeber*innen	Ruzica Piskac, Zvonimir Rakamarić
Verlag	Springer, Cham
Seiten	281-295
Seitenumfang	15
Auflage	1
ISBN (elektronisch)	978-3-031-98668-0
ISBN (Print)	978-3-031-98667-3
DOIs	https://doi.org/10.1007/978-3-031-98668-0_14
Publikationsstatus	Veröffentlicht - Juli 2025

Publikationsreihe

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

Wissenschaftszweige

102031 Theoretische Informatik
603109 Logik
102011 Formale Sprachen
102022 Softwareentwicklung
102001 Artificial Intelligence
202006 Computer Hardware
102 Informatik
101019 Stochastik
102003 Bildverarbeitung
103029 Statistische Physik
101018 Statistik
101017 Spieltheorie
202017 Embedded Systems
101016 Optimierung
101015 Operations Research
101014 Numerische Mathematik
101029 Mathematische Statistik
101028 Mathematische Modellierung
101026 Zeitreihenanalyse
101024 Wahrscheinlichkeitstheorie
102032 Computational Intelligence
102004 Bioinformatik
102013 Human-Computer Interaction
101027 Dynamische Systeme
305907 Medizinische Statistik
101004 Biomathematik
305905 Medizinische Informatik
101031 Approximationstheorie
102033 Data Mining
305901 Computerunterstützte Diagnose und Therapie
102019 Machine Learning
106007 Biostatistik
102018 Künstliche Neuronale Netze
106005 Bioinformatik
202037 Signalverarbeitung
202036 Sensorik
202035 Robotik

JKU-Schwerpunkte

Digital Transformation

Zugriff auf Dokument

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

Andere Dateien und Links

Verknüpfung zur Publikation in Scopus

Introducing Certificates to the Hardware Model Checking Competition
Froleyks, N. (Vortragende*r)
23 Juli 2025
Aktivität: Vortrag oder Präsentation › Vortrag nach Bewerbung und Auswahl › Science-to-science

CAV Distinguished Paper Award
Froleyks, N. (Empfänger*in), Yu, E. (Empfänger*in), Preiner, M. (Empfänger*in), Biere, A. (Empfänger*in) & Heljanko, K. (Empfänger*in), Juli 2025
Auszeichnung: Preis, Auszeichnung oder Ehrung

Dieses zitieren

Froleyks, N., Yu, E., Preiner, M., Biere, A., & Heljanko, K. (2025). Introducing Certificates to the Hardware Model Checking Competition. in R. Piskac, & Z. Rakamarić (Hrsg.), Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings: 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I (1 Aufl., S. 281-295). (Lecture Notes in Computer Science; Band 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. Hrsg. / Ruzica Piskac ; Zvonimir Rakamarić. 1. Aufl. Springer, Cham, 2025. S. 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ć (Hrsg.), Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings: 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I. 1 Aufl., Lecture Notes in Computer Science, Bd. 15931 LNCS, Springer, Cham, S. 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. Hrsg. / Ruzica Piskac; Zvonimir Rakamarić. 1. Aufl. Springer, Cham, 2025. S. 281-295 (Lecture Notes in Computer Science; Band 15931 LNCS).

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

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, Hrsg., Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings: 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I. 1 Aufl. Springer, Cham. 2025. S. 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

Publikationsreihe

Wissenschaftszweige

JKU-Schwerpunkte

Zugriff auf Dokument

Andere Dateien und Links

Aktivitäten

Introducing Certificates to the Hardware Model Checking Competition

Auszeichnungen

CAV Distinguished Paper Award

Dieses zitieren