Abstract
We present a comprehensive set of tactics that make it practical to use separation logic in a proof assistant. These tactics enable the verification of partial correctness properties of complex pointer-intensive programs. Our goal is to make separation logic as easy to use as the standard logic of a proof assistant. We have developed tactics for the simplification, rearranging, splitting, matching and rewriting of separation logic assertions as well as the discharging of a program verification condition using a separation logic description of the machine state. We have implemented our tactics in the Coq proof assistant, applying them to a deep embedding of Cminor, a C-like intermediate language used by Leroy’s verified CompCert compiler. We have used our tactics to verify the safety and completeness of a Cheney copying garbage collector written in Cminor. Our ideas should be applicable to other substructural logics and imperative languages.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, Washington, DC, USA, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)
Girard, J.Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: POPL 2005, pp. 220–231. ACM Press, New York (2004)
McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying gcs and their mutators. In: PLDI 2007, pp. 468–479. ACM, New York (2007)
The Coq Development Team: The Coq proof assistant, http://coq.inria.fr
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42–54. ACM Press, New York (2006)
Cheney, C.J.: A nonrecursive list compacting algorithm. Communications of the ACM 13(11), 677–678 (1970)
Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5–21. Springer, Heidelberg (2007)
Paulin-Mohring, C.: Inductive definitions in the system Coq—rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664. Springer, Heidelberg (1993)
Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 305–320. Springer, Heidelberg (2004)
Appel, A.W.: Tactics for separation logic (January 2006), http://www.cs.princeton.edu/~appel/papers/septacs.pdf
Marti, N., Affeldt, R., Yonezawa, A.: Formal verification of the heap manager of an os using separation logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 400–419. Springer, Heidelberg (2006)
Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515–529. Springer, Heidelberg (1997)
Myreen, M.O., Slind, K., Gordon, M.J.C.: Machine-code verification for multiple architectures - an application of decompilation into logic. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD) (2008)
Hawblitzel, C., Petrank, E.: Automated verification of practical garbage collectors. In: POPL 2009, pp. 441–453. ACM, New York (2009)
Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL 2007, pp. 97–108. ACM, New York (2007)
Marti, N., Affeldt, R.: A certified verifier for a fragment of separation logic. In: 9th JSSST Workshop on Programming and Prog. Langs, PPL 2007 (2007)
Tuerk, T.: A separation logic framework in HOL. In: Otmane Ait Mohamed, C.M., Tahar, S. (eds.) TPHOLs 2008: Emerging Trends Proceedings, August 2008, pp. 116–122 (2008)
Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL 2009, pp. 289–300. ACM, New York (2009)
Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Inf. Comput. 199(1-2), 200–227 (2005)
Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134–149. Springer, Heidelberg (2008)
Filliâtre, J.C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McCreight, A. (2009). Practical Tactics for Separation Logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2009. Lecture Notes in Computer Science, vol 5674. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03359-9_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-03359-9_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03358-2
Online ISBN: 978-3-642-03359-9
eBook Packages: Computer ScienceComputer Science (R0)