Introducing certificates to the hardware model checking competition
Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates to the hardware model checking competition. 37th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.
Download
Conference Paper
| Published
| English
Scopus indexed
Author
Froleyks, Nils;
Yu, EmilyISTA;
Preiner, Mathias;
Biere, Armin;
Heljanko, Keijo
Department
Series Title
LNCS
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.
Publishing Year
Date Published
2025-01-01
Proceedings Title
37th International Conference on Computer Aided Verification
Publisher
Springer Nature
Acknowledgement
This work is supported in part by the ERC-2020-AdG 101020093, the LIT AI Lab funded by the State of Upper Austria, the Research Council of Finland under the project 336092, and a gift from Intel Corporation.
Furthermore we of course also owe a big thank-you to the submitters of model checkers and benchmarks to the competition over all these years. Without their enthusiasm and support neither the competition nor this study would exist.
Volume
15931
Page
281-295
Conference
CAV: Computer Aided Verification
Conference Location
Zagreb, Croatia
Conference Date
2025-07-23 – 2025-07-25
ISBN
ISSN
eISSN
IST-REx-ID
Cite this
Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing certificates to the hardware model checking competition. In: 37th International Conference on Computer Aided Verification. Vol 15931. Springer Nature; 2025:281-295. doi:10.1007/978-3-031-98668-0_14
Froleyks, N., Yu, E., Preiner, M., Biere, A., & Heljanko, K. (2025). Introducing certificates to the hardware model checking competition. In 37th International Conference on Computer Aided Verification (Vol. 15931, pp. 281–295). Zagreb, Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-98668-0_14
Froleyks, Nils, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko. “Introducing Certificates to the Hardware Model Checking Competition.” In 37th International Conference on Computer Aided Verification, 15931:281–95. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-98668-0_14.
N. Froleyks, E. Yu, M. Preiner, A. Biere, and K. Heljanko, “Introducing certificates to the hardware model checking competition,” in 37th International Conference on Computer Aided Verification, Zagreb, Croatia, 2025, vol. 15931, pp. 281–295.
Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates to the hardware model checking competition. 37th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.
Froleyks, Nils, et al. “Introducing Certificates to the Hardware Model Checking Competition.” 37th International Conference on Computer Aided Verification, vol. 15931, Springer Nature, 2025, pp. 281–95, doi:10.1007/978-3-031-98668-0_14.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
2025_CAV_Froleyks.pdf
1.08 MB
Access Level
Open Access
Date Uploaded
2025-09-02
MD5 Checksum
15ec1bc9b9409d3b2736f4c9d5f42fd1
Google Scholar
ISBN Search