Inference of field-sensitive reachability and cyclicity
From MaRDI portal
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 which traverses the data structure on fld. In general, proving termination needs acyclicity, unless program-specific or non-automated 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 paper develops a static analysis inferring field-sensitive reachability and cyclicity information, which is more general than existing approaches. Propositional formulae 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 sub-trees, and "parent" to the parent node: termination of a loop traversing leaf-up cannot be guaranteed by state-of-the-art analyses. Instead, propositional formulae 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 paper defines the necessary abstract domains and builds an abstract semantics on them. A prototypical implementation provides the expected result on relevant examples.
Recommendations
- Reachability-based acyclicity analysis by abstract interpretation
- Verification, Model Checking, and Abstract Interpretation
- From shape analysis to termination analysis in linear time
- Cyclic proofs of program termination in separation logic
- Automatic Termination Proofs for Programs with Shape-Shifting Heaps
Cites work
- A semantics for procedure local heaps and its abstractions
- Automatic Termination Proofs for Programs with Shape-Shifting Heaps
- Cost analysis of object-oriented bytecode programs
- Cyclic proofs of program termination in separation logic
- scientific article; zbMATH DE number 1018876 (Why is no real title available?)
- scientific article; zbMATH DE number 1487860 (Why is no real title available?)
- Interprocedural shape analysis for effectively cutpoint-free programs
- Mechanical program analysis
- On the inference of resource usage upper and lower bounds
- Reachability-based acyclicity analysis by abstract interpretation
- Static Analysis
- Systematic design of program transformation frameworks by abstract interpretation
- The s-semantics approach: Theory and applications
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
Cited in
(2)
This page was built for publication: Inference of field-sensitive reachability and cyclicity
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946745)
