Abstract
Lightweight separation is a novel approach to automatic reasoning about memory updates in pointer programs. It replaces the spatial formulae of separation logic, which complicate automation, by independent assertions about the memory content and the memory layout. As a result, assertions about the content can be treated by existing reasoners. The effect of memory updates is evaluated using specialized tactics that prove disjointness of memory regions from a given memory layout. © 2008 Springer Berlin Heidelberg.
Cite
CITATION STYLE
Gast, H. (2008). Lightweight separation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5170 LNCS, pp. 199–214). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_18
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
