Emily Zhengqi Yu, Nils Froleyks, Armin Biere, Keijo Heljanko,
"Towards Compositional Hardware Model CheckingCertification"
, in Nadel, Alexander Rozier, Kristin Yvonne: Proceedings of the 23rd Conference on Formal Methods inComputer-Aided Design, Serie Conference Series: Formal Methods in Computer-Aided Design, TU Wien Academic Press, Seite(n) 44-54, 10-2023, ISBN: 978-3-85448-060-0
Original Titel:
Towards Compositional Hardware Model CheckingCertification
Sprache des Titels:
Englisch
Original Buchtitel:
Proceedings of the 23rd Conference on Formal Methods inComputer-Aided Design
Original Kurzfassung:
In this paper, we revisit and formalize temporaldecomposition, as one of the most basic, widely-used and effectivepreprocessing techniques in hardware model checking. The maincontribution is a certification framework for hardware modelchecking using temporal decomposition. Our approach enablesgeneration of a single inductive invariant in a compositional wayusing inductive invariant certificates provided by existingcertifying model checkers on the result of preprocessing a modelthrough temporal decomposition. We implement and evaluate the methodon hardware model checking competition benchmarks. The experimentsconfirm the effectiveness of temporal decomposition. The proposedcertification approach makes it feasible to generate a generic prooffor model checking and preprocessing
Sprache der Kurzfassung:
Englisch
Veröffentlicher:
TU Wien Academic Press
Serie:
Conference Series: Formal Methods in Computer-Aided Design