Abstract
We present a terminating shape analysis based on Separation Logic for programs that manipulate non-linear data structures such as trees and graphs. The analysis automatically calculates concise invariants for loops, with a level of precision depending on the manipulations applied on each program variable. We report experimental results obtained from running a prototype that implements our analysis on a variety of examples. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Cherini, R., Rearte, L., & Blanco, J. (2010). A shape analysis for non-linear data structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6337 LNCS, pp. 201–217). https://doi.org/10.1007/978-3-642-15769-1_13
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
