Abstract
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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM 52(6), 894–960 (2005); Preliminary version in POPL 2002
Barnett, M., DeLine, R., Fahndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Verification condition generation and variable conditions in Smallfoot, Available from: http://www.dcs.qmul.ac.uk/research/logic/theory/projects/smallfoot/index.html
Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005)
Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: 31st POPL, pp. 220–231 (2004)
Bornat, R., Calcagno, C., O’Hearn, P.: Local reasoning, separation, and aliasing. In: 2nd SPACE Workshop (2004)
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: 32nd POPL, pp. 59–70 (2005)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
Brinch-Hansen, P. (ed.): The Origin of Concurrent Programming. Springer, Heidelberg (2002)
Brookes, S.D.: A semantics for concurrent separation logic (Priliminary Version). In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 16–34. Springer, Heidelberg (2004)
Clarke, D., Noble, J., Potter, J.: Simple ownership types for object containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 53–76. Springer, Heidelberg (2001)
DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: 8th PLDI, pp. 59–69 (2001)
Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (2006)
Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: Le Métayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol. 2305, pp. 262–277. Springer, Heidelberg (2002)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: 9th PLDI, pp. 234–245 (2002)
Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Engeler, E. (ed.) Symposium on the Semantics of Algorithmic Languages. Lecture Notes in Mathematics, vol. 188, pp. 102–116. Springer, Heidelberg (1971)
Hoare, C.A.R.: Towards a theory of parallel programming. In: Operating Systems Techniques, pp. 61–71. Acad. Press, London (1972); Reprinted in [10]
Jacobs, B., Leino, K.R.M., Piessens, F., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: 3rd SEFM (2005)
Jenson, J., Jorgensen, M., Klarkund, N., Schwartzback, M.: Automatic verification of pointer programs using monadic second-order logic. In: 4th PLDI, pp. 225–236 (1997)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Conf. (1983)
Jones, C.B.: Wanted: A compositional approach to concurrency. In: McIver, A., Morgan, C. (eds.) Programming Methodology, pp. 1–15. Springer, Heidelberg (2003)
Knuth, D.E.: The Art of Computer Programming, 2nd edn. Fundamental Algorithms, vol. I. Addison-Wesley, Reading (1973)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–515. Springer, Heidelberg (2004)
Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: 9th PLDI, pp. 246–257 (2002)
Michael, M.M.: Hazard pointers: Safe memory reclamation for lock-free objects. IEEE TPDS 15(6), 491–504 (2004)
Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417–426 (1981)
Möller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: 8th PLDI, pp. 221–231 (2001)
Naumann, D.A.: Assertion-based encapsulation, invariants and simulations. In: 3rd FMCO, pp. 251–273 (2005)
Naumann, D.A., Barnett, M.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 54–84. Springer, Heidelberg (2004)
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science (to appear, 2006); Preliminary version in CONCUR 2004
O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: 31st POPL, pp. 268–280 (2004)
Parkinson, M., Bornat, R.: Exploiting linearisability in program logic. Draft paper (2005)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55–74
Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., Wilhelm, R.: A semantics for procedure local heaps and its abstractions. In: 32nd POPL, pp. 296–309 (2005)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS 24(3), 217–298 (2002)
Schwarz, J.: Generic commands—A tool for partial correctness formalisms. The Computer Journal 20(2), 151–155 (1977)
Walker, D., Morrisett, J.G.: Alias types for recursive data structures. In: 3rd Types in Compilation Workshop, pp. 177–206 (2001)
Yang, H.: An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. In: 1st SPACE Workshop (2001)
Yang, H., O’Hearn, P.W.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berdine, J., Calcagno, C., O’Hearn, P.W. (2006). Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2005. Lecture Notes in Computer Science, vol 4111. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11804192_6
Download citation
DOI: https://doi.org/10.1007/11804192_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-36749-9
Online ISBN: 978-3-540-36750-5
eBook Packages: Computer ScienceComputer Science (R0)