Abstract interpretation with a congruence abstract domain and/or a heap succession abstract domain
First Claim
1. A tool comprising software for tracking equivalence classes between plural alien expressions and plural base domain variables.
2 Assignments
0 Petitions
Accused Products
Abstract
Techniques and tools are described for analyzing software. For example, an analysis tool performs abstract interpretation with a congruence abstract domain and/or a heap succession abstract domain. For the congruence abstract domain, the tool tracks equivalence classes between alien expressions and base domain variables. For the heap succession abstract domain, the tool tracks updates to a heap. In either case, to preserve information after updates, the tool may identify an expression having an unreachable value then determine an equivalent expression that lacks the unreachable value.
-
Citations
20 Claims
- 1. A tool comprising software for tracking equivalence classes between plural alien expressions and plural base domain variables.
-
11. A method comprising:
-
identifying for an abstract domain an expression having one or more unreachable values; and
determining an equivalent expression that lacks the one or more unreachable values. - View Dependent Claims (12, 13, 14, 15)
-
- 16. A method comprising, in an abstract domain, tracking one or more updates to a memory pool, wherein software implementing the abstract domain facilitates replacement of expressions having one or more unreachable values.
Specification