Introducing Certificates to the Hardware Model Checking Competition

Description

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.

Period	23 Jul 2025
Event title	37th International Conference on Computer Aided Verification
Event type	Conference
Conference number	37
Location	Zagreb, CroatiaShow on map
Degree of Recognition	International