Liveness Proofs for Hardware Model Checking

Lecture notes in computer science, pp. 3–27

Abstract

Abstract We introduce a generic certificate format for verifying liveness properties in hardware model checking. The format relies purely on propositional predicates and does not involve explicit counters. Our certificates can be efficiently validated using a fixed number of SAT checks. The proposed format is compatible with state-of-the-art liveness checking algorithms. We present certificate generation for several representative techniques, including rLive, liveness-to-safety reduction, and k -liveness, as well as for a preprocessing method based on stabilizing constraint extraction. Experimental results on benchmarks from the Hardware Model Checking Competition demonstrate that our approach is practically effective with very low certification overhead, and our certificate checker successfully validated all generated certificates.

Authors 5

1. Nils Froleyks corresponding

   KU Leuven

   Affiliation as printed

   KU Leuven, Leuven, Belgium

2. Emily Yu Aachen

   Leiden University

   Affiliation as printed

   Leiden University, Leiden, Netherlands

3. Bart Bogaerts

   KU Leuven

   Affiliation as printed

   KU Leuven, Leuven, Belgium

4. Armin Biere

   University of Freiburg

   Affiliation as printed

   University of Freiburg, Freiburg, Germany

5. Keijo Heljanko

   University of Helsinki · Helsinki Institute for Information Technology

   Affiliation as printed

   Helsinki Institute for Information Technology, Helsinki, Finland

   University of Helsinki, Helsinki, Finland