Separation logic is a program logic for reasoning about programs that manipulate pointer data structures. We describe Smallfoot, a tool for checking certain lightweight separation logic specifications. The assertions describe the shapes of data structures rather than their detailed contents, and this allows reasoning to be fully automatic. The presentation in the paper is tutorial in style. We illustrate what the tool can do via examples which are oriented toward novel aspects of separation logic, namely: avoidance of frame axioms (which say what a procedure does not change); embracement of "dirty" features such as memory disposal and address arithmetic; information hiding in the presence of pointers; and modular reasoning about concurrent programs. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Berdine, J., Calcagno, C., & O’Hearn, P. W. (2006). Smallfoot: Modular automatic assertion checking with separation logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4111 LNCS, pp. 115–137). Springer Verlag. https://doi.org/10.1007/11804192_6
Mendeley helps you to discover research relevant for your work.