Towards Compositional Hardware Model Checking Certification
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
Conference on Formal Methods in Computer-Aided Design 2023
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
We revisit and formalize temporal decomposition, as one of the most basic, widely-used and effective preprocessing techniques in hardware model checking. The main contribution is a certification framework for hardware model checking using temporal decomposition. Our approach enables generation of a single inductive invariant in a compositional way using inductive invariant certificates provided by existing certifying model checkers on the result of preprocessing a model through temporal decomposition. We implement and evaluate the method on hardware model checking competition benchmarks. The experiments confirm the effectiveness of temporal decomposition. The proposed certification approach makes it feasible to generate a generic proof for model checking and preprocessing
Forschungs-