nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Backwards and Forwards with Separation Logic

verfasst von : Callum Bannister, Peter Höfner, Gerwin Klein

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The use of Hoare logic in combination with weakest preconditions and strongest postconditions is a standard tool for program verification, known as backward and forward reasoning. In this paper we extend these techniques to allow backward and forward reasoning for separation logic. While the former is derived directly from the standard operators of separation logic, the latter uses a new one. We implement our framework in the interactive proof assistant Isabelle/HOL, and enable automation with several interactive proof tactics.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Software Tool Support for Modular Reasoning in Modal Logics of Actions

Nächstes Kapitel A Coq Formalisation of SQL’s Execution Engines

We will explain the heap model in detail later in this section.

Updated proofs at https://github.com/seL4/l4v/tree/seL4-7.0.0/sys-init.

Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_1CrossRef

Appel, A.W.: VeriSmall: verified smallfoot shape analysis. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 231–246. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25379-9_18CrossRef

Bannister, C., Höfner, P., Klein, G.: Forward and backward reasoning in separation logic. Isabelle theories (2018). https://github.com/sel4proj/Jormungand/tree/ITP18

Bengtson, J., Jensen, J.B., Birkedal, L.: Charge! A framework for higher-order. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 315–331. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_21CrossRef

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). https://doi.org/10.1007/11575467_5CrossRef

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5

Boyton, A., Andronick, J., Bannister, C., Fernandez, M., Gao, X., Greenaway, D., Klein, G., Lewis, C., Sewell, T.: Formally verified system initialisation. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 70–85. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41202-8_6CrossRef

Burstal, R.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 23–50. Edinburgh University Press, Edinburgh (1972)

Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26:1–26:66 (2011). https://doi.org/10.1145/2049697.2049700

10.

Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Logic in Computer Science (LICS 2007), pp. 366–378. IEEE (2007). https://doi.org/10.1109/LICS.2007.30

11.

Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108–119. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45294-X_10CrossRef

12.

Charguéraud, A.: Characteristic formulae for the verification of imperative programs. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) International Conference on Functional Programming (ICFP 2011), pp. 418–430. ACM (2011). https://doi.org/10.1145/2034773.2034828

13.

Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: Hall, M.W., Padua, D.A. (eds.) Programming Language Design and Implementation (PLDI 2011), pp. 234–245. ACM (2011). https://doi.org/10.1145/1993498.1993526

14.

Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167–182. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_16CrossRef

15.

Dang, H.H., Höfner, P., Möller, B.: Algebraic separation logic. J. Logic Algebraic Programm. 80(6), 221–247 (2011). https://doi.org/10.1016/j.jlap.2011.04.003CrossRefMATH

16.

Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Upper Saddle River (1976)

17.

Distefano, D., Filipović, I.: Memory leaks detection in java by bi-abductive inference. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 278–292. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12029-9_20CrossRef

18.

Distefano, D., O’Hearn, P.W., 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). https://doi.org/10.1007/11691372_19CrossRefMATH

19.

Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci. 19, 19–32 (1967)MathSciNetCrossRef

20.

Gordon, M., Collavizza, H.: Forward with hoare. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, pp. 101–121. Springer, London (2010). https://doi.org/10.1007/978-1-84882-912-1_5CrossRefMATH

21.

Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259CrossRefMATH

22.

Hobor, A., Villard, J.: The ramifications of sharing in data structures. In: Giacobazzi, R., Cousot, R. (eds.) Principles of Programming Languages (POPL 2013), pp. 523–536. ACM (2013). https://doi.org/10.1145/2429069.2429131

23.

Hóu, Z., Goré, R., Tiu, A.: Automated theorem proving for assertions in separation logic with all connectives. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 501–516. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_34CrossRefMATH

24.

Hóu, Z., Sanán, D., Tiu, A., Liu, Y.: Proof tactics for assertions in separation logic. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 285–303. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66107-0_19CrossRef

25.

Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Principles of Programming Languages (POPL 2001), vol. 36, pp. 14–26. ACM (2001). https://doi.org/10.1145/373243.375719

26.

Jacobs, B., Smans, J., Piessens, F.: A quick tour of the verifast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304–311. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17164-2_21CrossRef

27.

Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Principles of Programming Languages (POPL 2015), pp. 637–650. ACM (2015). https://doi.org/10.1145/2676726.2676980

28.

Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. Trans. Comput. Syst. 32(1), 2:1–2:70 (2014). https://doi.org/10.1145/2560537

29.

Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 332–337. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_22CrossRef

30.

Klein, G., Kolanski, R., Boyton, A.: Separation algebra. Archive of Formal Proofs, Formal proof development (2012). http://isa-afp.org/entries/Separation_Algebra.shtml

31.

Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D. (eds.) Principles of Programming Languages (POPL 2017), pp. 205–217. ACM (2017). https://doi.org/10.1145/3009837.3009855

32.

Lee, W., Park, S.: A proof system for separation logic with magic wand. In: Jagannathan, S., Sewell, P. (eds.) Principles of Programming Languages (POPL 2014), pp. 477–490. ACM (2014). https://doi.org/10.1145/2535838.2535871

33.

Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20CrossRefMATH

34.

Maclean, E., Ireland, A., Grov, G.: Proof automation for functional correctness in separation logic. J. Logic Comput. 26(2), 641–675 (2016). https://doi.org/10.1093/logcom/exu032MathSciNetCrossRefMATH

35.

Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 121–135. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45085-6_10CrossRef

36.

Nipkow, T.: Hoare logics in Isabelle/HOL. In: Schwichtenberg, H., Steinbrüggen, R. (eds.) Proof and System-Reliability, pp. 341–367. Springer, Heidelberg (2002). https://doi.org/10.1007/978-94-010-0413-8_11

37.

Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9CrossRefMATH

38.

O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44802-0_1CrossRef

39.

Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science (LICS 2002), pp. 55–74 (2002). https://doi.org/10.1109/LICS.2002.1029817

40.

Reynolds, J.C.: An introduction to separation logic. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 22, pp. 285–310. IOS Press (2009). https://doi.org/10.3233/978-1-58603-976-9-285

41.

Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Grove, D., Blackburn, S. (eds.) Programming Language Design and Implementation (PLDI 2015), pp. 77–87. ACM (2015). https://doi.org/10.1145/2737924.2737964

42.

Tuerk, T.: A Separation Logic Framework for HOL. Ph.D. thesis, University of Cambridge, UK (2011)

43.

Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_18CrossRef

Titel: Backwards and Forwards with Separation Logic
verfasst von: Callum Bannister
Peter Höfner
Gerwin Klein
Verlag: Springer International Publishing
Buch: Interactive Theorem Proving
Print ISBN: 978-3-319-94820-1

Electronic ISBN: 978-3-319-94821-8

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-94821-8_5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner