Clause and Proof Tightening
OwnerOded Fuhrmann, Ohad Shacham +2inventors
InventorsOded Fuhrmann, Ohad Shacham, Ofer Strichman, Tatyana Veksler
Life of this patent
Estimating the term…
Abstract
A computer-implemented method for verification of a target system includes defining a formula describing the target system, the formula including clauses, which include variables and which express constraints on states of the target system. The formula is processed so as to derive, using the clauses, a proof relating to a property of the target system. After deriving the proof, a variable that has a constant value is identified in the proof. The number of the variables in the proof is reduced using the identified variable, thereby producing a tightened expression, which is applied in making a determination of whether the target system satisfies the formula.
Claims20
A computer-implemented method for verification of a target system, the method comprising:
- defining a formula describing the target system, the formula comprising clauses, which comprise variables and which express constraints on states of the target system;
- processing the formula so as to derive, using the clauses, a proof relating to a property of the target system;
- after deriving the proof, identifying a variable in the proof that has a constant value;
- reducing a number of the variables in the proof using the identified variable, thereby producing a tightened expression;
- applying the tightened expression in making a determination of whether the target system satisfies the formula;
- and
- generating an output indicative of a verification status of the target system responsively to the determination.
Apparatus for verification of a target system, the apparatus comprising:
- a memory, which is arranged to store a formula describing the target system, the formula comprising clauses, which comprise variables and which express constraints on states of the target system;
- and
- a processor, which is configured to process the formula so as to derive, using the clauses, a proof relating to a property of the target system, and after deriving the proof, to identify a variable in the proof that has a constant value, to reduce the number of the variables in the proof using the identified variable, thereby producing a tightened expression, and to apply the tightened expression in making a determination of whether the target system satisfies the formula.
A computer software product for verification of a target system, the product comprising a computer-readable medium in which program instructions are stored, which instructions, when read by a computer, cause the computer to accept a formula describing the target system, the formula comprising clauses, which comprise variables and which express constraints on states of the target system, and to process the formula so as to derive, using the clauses, a proof relating to a property of the target system, and after deriving the proof, to identify variable in the proof that has a constant value, to reduce the number of the variables in the proof using the identified variable, thereby producing a tightened expression, and to apply the tightened expression in making a determination of whether the target system satisfies the formula.
Dependencies are inferred from the claim text.