Identifying invariant candidates based on proofs

摘要

Candidate invariants are selected from a proof of a property. In some exemplary embodiments, a proof of a property with respect to a bounded model having a bounded number of cycles may be obtained. The bounded model may comprise an initial axiom and a transition relation axiom. The proof of the property is a Directed Acyclic Graph (DAG). Each non-leaf node of the DAG is deducible from its child nodes. A root of the DAG is the property. Leaves of the DAG are associated with an axiom of the bounded model. A set of candidate invariants may be selected from the DAG. A subset of the set of candidates may be determined such that the subset comprises invariants which are held during each cycle of an unbounded model, wherein the unbounded model is an unbounded version of the bounded model. The invariants may be utilized for model checking of the unbounded model.