Reachability analysis for program verification
AssigneeNEC Laboratories America, Inc.
InventorsChao Wang, Zijiang Yang, Aarti Gupta
Life of this patent
Estimating the term…
Abstract
An improved method for automatically improving the precision of an extrapolation operator used, for example, in software program verification in connection with the static analysis and model checking of the software programs which rely on fix-point computation. In particular, a new extrapolation-with-care-set operator, together with a method for gradually increasing the precision of this operation by tightening the care set.
Claims6
An improvement to a computer-implemented method to perform a static analysis on a software program using a fix-point computation using pre-condition or post-condition operations, wherein said method employs an extrapolation operation to accelerate the convergence of the method, wherein said improvement is CHARACTERIZED IN THAT:
- the extrapolation employs a care-set that identifies one or more forbidden areas of extrapolation;
- and
- outputs an indication of those forbidden areas;
- wherein the extrapolation is performed on convex polyhedra, and P,Q are two polyhedra, and C is a powerset such that Q∩C=Ø wherein the extrapolation of P with respect to Q under the care set C is computed according to the following steps:
- building a new polyhedron P′ for each constraint c of P whose half-space does not contain Q, such that if Pc∩C=└ then c is dropped;
- building a new polyhedron Q′ by dropping any constraint c of Q whose half-space does not contain P′;
- and
- returning Q′ as the result of the extrapolation.
An improved computer implemented method to perform a backward reachability analysis which produces a set of reachable states represented as polyhedra wherein the improvement comprises:
- simplifying the polyhedral representation of pre-image sets through the use of restricts;
- and
- outputs an indication of the set of reachable states;
- wherein given two sets P and Q, the restrict P↓Q is determined to be a new set {x∈Zn|x∈P∩Q, or x∉Q};
- wherein P and Q are convex polyhedra and (P↓Q) is determined according to the following steps:
- If P=Zn or if Q=Ø, return Zn;
- Otherwise, in the recursive step, choose a constraint c from P:
- if c∩Q is empty, return (Pc↓Q), else return c∩(Pc↓(Q∩c)).
Dependencies are inferred from the claim text.