Parametric shape analysis via 3-valued logic
University of Wisconsin–Madison · Tel Aviv University · +1 more institution
Abstract
Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This article presents a parametric framework for shape analysis that can be instantiated in different ways to create different shape-analysis algorithms that provide varying degrees of efficiency and precision. A key innovation of the work is that the stores that can possibly arise during execution are represented (conservatively) using 3-valued logical structures. The framework is instantiated in different ways by varying the predicates used in the 3-valued logic. The class of programs to which a given instantiation of the framework can be applied is not…
Citation impact
- FWCI
- 56.71
- Percentile
- 100%
- References
- 44
Authors
3Topics & keywords
- Computer science
- A priori and a posteriori
- Parametric statistics
- Set (abstract data type)
- Key (lock)
- Shape analysis (program analysis)
- Program analysis
- Programming language
- Industry, innovation and infrastructure