DONUT DOMAINS - EFFICIENT NON-CONVEX DOMAINS FOR ABSTRACT INTERPRETATION
First Claim
3-1. The method of claim 3 wherein said regions are ones selected from the group consisting of:
- intervals, octagons, and polyhedra.
3 Assignments
0 Petitions
Accused Products
Abstract
A computer implemented program analysis method employing a set of new abstract domains applicable to non-convex invarients. The method analyzes programs statically using abstract interpretation while advantageously considering non-convex structures and in particular those situations in which an internal region of an unreachable state exists within a larger region of reachable states. The method employs a new set of non-convex domains (donut domains) based upon the notion of an outer convex region of reachable states (Domain D1) and an inner region of unreachable states (Domain D2) which advantageously permits capture of non-convex properties by using convex regions and operations.
8 Citations
20 Claims
-
3-1. The method of claim 3 wherein said regions are ones selected from the group consisting of:
- intervals, octagons, and polyhedra.
- 6. The method of claim 6 further comprising the step of using an LP-solver to find matrix Λ
-
10. A computer implemented method for determining a maximal inner polyhedron ={x ∈
-
p|Tx≦
c} of a given template matrix T that lies within a given non-empty polyhedron ={x ∈
p|Ax≦
b}, comprising the steps of;computing an auxiliary matrix A with non-negative elements and Λ
T=A,computing c such that Λ
c≦
b and Tx≦
c is consistent,and outputting such inner polyhedron . - View Dependent Claims (11, 12, 13, 14, 15)
-
p|Tx≦
-
16. A computer system comprising program instructions adapted to be executed for computer program analysis, said instructions being stored in computer-readable memory, and when executed by the computer system cause the computer system to be operable to:
-
generate an outer convex region of all reachable states for the computer program wherein the outer region (D1) represents an over-approximation of all of the reachable states; generate an inner convex region of all unreachable states for the computer program wherein the inner region (D2) represents an under-approximation of all of the unreachable states; and generate a set of possible program errors using abstract interpretation over the difference between the two regions. - View Dependent Claims (17, 18, 19, 20)
-
Specification