Name
Abstract | ||
|---|---|---|
In heap-based languages, knowing that a variable x points to an acyclic data structure is useful for analyzing termination. This information guarantees that the depth of the data structure to which x points is greater than the depth of the structure pointed to by x.fld, and allows bounding the number of iterations of a loop that traverses the data structure on fld. In general, proving termination needs acyclicity, unless program-specific or nonautomated reasoning is performed. However, recent work could prove that certain loops terminate even without inferring acyclicity, because they traverse data structures “acyclically.” Consider a double-linked list: if it is possible to demonstrate that every cycle involves both the “next” and the “prev” field, then a traversal on “next” terminates since no cycle will be traversed completely. This article develops a static analysis inferring field-sensitive reachability and cyclicity information, which is more general than existing approaches. Propositional formulæ are computed, which describe which fields may or may not be traversed by paths in the heap. Consider a tree with edges “left” and “right” to the left and right subtrees, and “parent” to the parent node: termination of a loop traversing leaf-up cannot be guaranteed by state-of-the-art analyses. Instead, propositional formulæ computed by this analysis indicate that cycles must traverse “parent” and at least one between “left” and “right”: termination is guaranteed, as no cycle is traversed completely. This work defines the necessary abstract domains and builds an abstract semantics on them. A prototypical implementation provides the expected result on relevant examples. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2629478 | ACM Trans. Comput. Log. |
Keywords | Field | DocType |
cyclicity analysis,pointer analysis,abstract interpretation,specifying and verifying and reasoning about programs,mathematical logic,data structures,shape analysis,verification,software/program verification,automatic programming,static analysis,termination analysis,theory,heap manipulation,semantics of programming languages | Discrete mathematics,Pointer analysis,Data structure,Combinatorics,Tree traversal,Abstract interpretation,Algorithm,Heap (data structure),Reachability,Termination analysis,Mathematics,Traverse | Journal |
Volume | Issue | ISSN |
15 | 4 | 1529-3785 |
Citations | PageRank | References |
1 | 0.35 | 29 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Damiano Zanardini | 1 | 324 | 16.83 |
| Samir Genaim | 2 | 891 | 44.31 |