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.

主权项

1. A computer-implemented method performed by a computerized device, comprising:
obtaining a proof of a property with respect to a bounded model having a bounded number of cycles, wherein the bounded model comprising an initial axiom and a transition relation axiom, wherein the proof of the property is a Directed Acyclic Graph (DAG), wherein each non-leaf node of the DAG is deducible from its child nodes, wherein a root of the DAG is the property, and wherein leaves of the DAG are associated with an axiom of the bounded model; selecting a set of candidate invariants comprising at least one intermediate node of the DAG; determining, without using the proof and using a Boolean satisfiability problem solver, a subset of the set of candidates, wherein the subset comprises invariants which are held in an unbounded model during each cycle after the bound, wherein the unbounded model is an unbounded version of the bounded model; and utilizing the subset for model checking of the unbounded model.