# zbMATH — the first resource for mathematics

Separation logic tutorial. (English) Zbl 1185.68228
Garcia de la Banda, Maria (ed.) et al., Logic programming. 24th international conference, ICLP 2008, Udine, Italy, December 9–13 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-89981-5/pbk). Lecture Notes in Computer Science 5366, 15-21 (2008).
Summary: Separation logic is an extension of Hoare’s logic for reasoning about programs that manipulate pointers. It is based on the separating conjunction $$P \ast Q$$, which asserts that $$P$$ and $$Q$$ hold for separate portions of computer memory.
This tutorial on separation logic has three parts.
1. Basics: Concentrating on highlights from the early work.
2. Model Theory: The model theory of separation logic evolved from the general resource models of bunched logic and includes an account of program dynamics in terms of their interaction with resource.
3. Proof Theory: I describe the aspects of proof theory, in particular new entailment questions (frame and anti-frame inference), which are important for applications in mechanized program verification.
For the entire collection see [Zbl 1154.68013].
Reviewer: Reviewer (Berlin)
##### MSC:
 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 03B70 Logic in computer science 68Q60 Specification and verification (program logics, model checking, etc.)
##### Software:
jStar; Smallfoot; THOR
Full Text:
##### References:
 [1] Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Millennial Perspectives in Computer Science. Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare, Palgrave, pp. 303–321 (2000) [2] Isthiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: 28th POPL, pp. 36–49 (2001) [3] O’Hearn, P., Reynolds, J., 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) · Zbl 0999.68045 · doi:10.1007/3-540-44802-0_1 [4] Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55–74 (2002) [5] O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999) · Zbl 0930.03095 · doi:10.2307/421090 [6] Pym, D.J.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer Academic Publishers, Dordrecht (2002) · Zbl 1068.03001 · doi:10.1007/978-94-017-0091-7 [7] Pym, D., O’Hearn, P., Yang, H.: Possible worlds and resources: the semantics of BI. Theoretical Computer Science 315(1), 257–305 (2004) · Zbl 1055.03021 · doi:10.1016/j.tcs.2003.11.020 [8] Yang, H., O’Hearn, P.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002) · Zbl 1077.68705 · doi:10.1007/3-540-45931-6_28 [9] Calcagno, C., O’Hearn, P., Yang, H.: Local action and abstract separation logic. In: 22nd LICS, pp. 366–378 (2007) · doi:10.1109/LICS.2007.30 [10] Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780. Springer, Heidelberg (2005) · Zbl 1159.68363 · doi:10.1007/11575467_5 [11] Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis. Imperial College DOC Tech. Report 2008/12 [12] Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Automatic modular assertion checking with separation logic. In: 4th FMCO, pp. 115–137 (2006) [13] Distefano, D., O’Hearn, P., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006) · Zbl 1180.68112 · doi:10.1007/11691372_19 [14] Magill, S., Nanevski, A., Clarke, E., Lee, P.: Inferring invariants in Separation Logic for imperative list-processing programs. In: 3rd SPACE Workshop (2006) [15] Berdine, J., Cook, B., Distefano, D., O’Hearn, P.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386–400. Springer, Heidelberg (2006) · Zbl 1188.68109 · doi:10.1007/11817963_35 [16] Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI 2007 (2007) · doi:10.1145/1250734.1250765 [17] Guo, B., Vachharajani, N., August, D.: Shape analysis with inductive recursion synthesis. In: PLDI (2007) · doi:10.1145/1250734.1250764 [18] Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T., Yang, H.: Shape analysis of composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590. Springer, Heidelberg (2007) · Zbl 1135.68372 · doi:10.1007/978-3-540-73368-3_22 [19] Magill, S., Tsai, M.-S., Lee, P., Tsay, Y.-K.: THOR: A tool for reasoning about shape and arithmetic. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123. Springer, Heidelberg (2008) · Zbl 05301131 · doi:10.1007/978-3-540-70545-1_41 [20] 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) · Zbl 1369.68154 · doi:10.1145/1040305.1040330 [21] Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 240–260. Springer, Heidelberg (2006) · Zbl 1225.68072 · doi:10.1007/11823230_16 [22] Nguyen, H.H., Chin, W.-N.: Enhancing program verification with lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123. Springer, Heidelberg (2008) · Zbl 1155.68443 · doi:10.1007/978-3-540-70545-1_34 [23] Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123. Springer, Heidelberg (2008) · Zbl 1155.68359 · doi:10.1007/978-3-540-70545-1_36 [24] Distefano, D., Parkinson, M.: jStar: Towards Practical Verification for Java. In: OOPSLA (2008) [25] Marti, N., Affeldt, R., Yonezawa, A.: Verification of the heap manager of an operating system using separation logic. In: 3rd SPACE Workshop (2006) · doi:10.1007/11901433_22 [26] Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: 34th POPL, pp. 97–108 (2007) · Zbl 1295.68094 · doi:10.1145/1190216.1190234 [27] Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424. Springer, Heidelberg (2007) · Zbl 1186.68118 · doi:10.1007/978-3-540-71209-1_44 [28] Gardner, P., Smith, G., Wheelhouse, M., Zarfaty, U.: Local Hoare reasoning about DOM. In: 27th PODS, pp. 261–270 (2008) · doi:10.1145/1376916.1376953 [29] Parkinson, M., Bierman, G.: Separation logic and abstraction. In: 32nd POPL, pp. 59–70 (2005) · Zbl 1369.68151 · doi:10.1145/1040305.1040326 [30] O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science (Reynolds Festschrift) 375(1-3), 271–307 (2007) · Zbl 1111.68023 · doi:10.1016/j.tcs.2006.12.035 [31] Brookes, S.D.: A semantics of concurrent separation logic. Theoretical Computer Science (Reynolds Festschrift) 375(1-3), 227–270 (2007) · Zbl 1111.68021 · doi:10.1016/j.tcs.2006.12.034
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.