A static shape analysis is presented that can prove the absence of NULL- and dangling pointer dereferences in standard algorithms on lists, trees and graphs. It is conceptually simpler than other analyses that use symbolically represented logic to describe the heap. Instead, it represents the heap as a single graph and a Boolean formula. The key idea is to summarize two nodes by calculating their common points-to information, which is done using the recently proposed fold and expand operations. The force of this approach is that both, fold and expand, retain relational information between points-to edges, thereby essentially inferring new shape invariants. We show that highly precise shape invariants can be inferred using off-the-shelf SAT-solvers. Cheaper approximations may augment standard points-to analysis used in compiler optimisations. © 2013 Springer-Verlag.
CITATION STYLE
Siegel, H., & Simon, A. (2013). FESA: Fold- and expand-based shape analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7791 LNCS, pp. 82–101). https://doi.org/10.1007/978-3-642-37051-9_5
Mendeley helps you to discover research relevant for your work.