| 摘要 |
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.
|
