Abstract
The driving force behind Space Invader [1,2,3] - an automatic tool aiming to perform accurate static analysis of programs using pointers - is the idea of local reasoning, which is enabled by the Frame Rule of separation logic [4]: In this rule R is the frame, i.e., the part of the heap which is not touched by the execution of the command C. The Frame Rule allows pre and postconditions to concentrate on the footprint: the cells touched by command C. © 2008 Springer Berlin Heidelberg.
Cite
CITATION STYLE
Distefano, D. (2008). Abductive inference for reasoning about heaps. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5356 LNCS, pp. 1–2). Springer Verlag. https://doi.org/10.1007/978-3-540-89330-1_1
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
