Certifying rlive: A New Proof Strategy for Liveness Model Checking

SAT-based model checking has become a prominent approach to the verification of temporal properties. However, while invariant model checking can produce simple proofs based on induction, proof generation for SAT-based model checking of liveness properties is much more complex. In this paper, we focus on a recently developed algorithm, called rlive, which has been proved quite effective in practice. rlive tries to find a counterexample with a series of reachability checks, while iteratively blocking shoals, i.e., set of states that cannot be extended with fair paths. Despite the complexity of the algorithm, we show that the shoals are sufficient to generate a proof in a deductive system for temporal properties. We implement the approach in an existing certifying model checking framework based on the PVS theorem prover, and we experimentally evaluate it on liveness verification problems from the hardware model checking competition, generating proofs using the nuXmv model checker and checking them with PVS.