Abstract
This paper extends Reynolds’ separation logical system for pointer-based while program verification by adding inductive definitions. Inductive definitions give us a great advantage for verification, since they enable us for example, to formalize linked lists and to support the lemma reasoning mechanism. This paper proves its completeness theorem that states that every true asserted program is provable in the logical system. In order to prove its completeness, this paper shows an expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion.
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
Apt, K.R.: Ten Years of Hoare’s Logic: A Survey — Part I. ACM Transactions on Programming Languages and Systems 3(4), 431–483 (1981)
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)
Bergstra, J.A., Tucker, J.V.: Expressiveness and the Completeness of Hoare’s Logic. Journal Computer and System Sciences 25(3), 267–284 (1982)
Brotherston, J.: Formalised Inductive Reasoning in the Logic of Bunched Implications. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 87–103. Springer, Heidelberg (2007)
Brotherston, J., Villard, J.: Parametric Completeness for Separation Theories. In: Proceedings of POPL 2014, pp. 453–464 (2014)
Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing 7(1), 70–90 (1978)
Coquand, T., Paulin, C.: Inductively Defined Types. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990)
Halpern, J.Y.: A good Hoare axiom system for an ALGOL-like language. In: Proceedings of POPL 1984, pp. 262–271 (1984)
Hou, Z., Clouston, R., Gore, R., Tiu, A.: Proof search for propositional abstract separation logics via labelled sequents. In: Proceedings of POPL 2014, pp. 465–476 (2014)
Josko, B.: On expressive interpretations of a Hoare-logic for Clarke’s language L4. In: Fontet, M., Mehlhorn, K. (eds.) STACS 1984. LNCS, vol. 166, pp. 73–84. Springer, Heidelberg (1984)
Kimura, D., Tatsuta, M.: Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types. Logical Methods in Computer Science 9(1), Article 14 (2013)
Lee, W., Park, S.: A Proof System for Separation Logic with Magic Wand. In: Proceedings of POPL 2014, pp. 477–490 (2014)
Nguyen, H.H., David, C., Qin, S.C., Chin, W.N.: Automated Verification of Shape and Size Properties Via Separation Logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007)
Nguyen, H.H., Chin, W.N.: Enhancing Program Verification with Lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 355–369. Springer, Heidelberg (2008)
Paulin-Mohring, C.: Extracting F ω ’s programs from proofs in the Calculus of Constructions. In: Proceedings of POPL 1989, pp. 89–104 (1989)
Pohlers, W.: Proof Theory. Springer (2009)
Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proceedings of LICS 2002, pp. 55–74 (2002)
Tatsuta, M.: Program synthesis using realizability. Theoretical Computer Science 90, 309–353 (1991)
Tatsuta, M., Chin, W.N., Al Ameen, M.F.: Completeness of Pointer Program Verification by Separation Logic. In: Proceeding of SEFM 2009, pp. 179–188 (2009)
Tatsuta, M., Chin, W.N., Al Ameen, M.F.: Completeness of Pointer Program Verification by Separation Logic. NII Technical Report, NII-2009-013E (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Tatsuta, M., Chin, WN. (2014). Completeness of Separation Logic with Inductive Definitions for Program Verification. In: Giannakopoulou, D., Salaün, G. (eds) Software Engineering and Formal Methods. SEFM 2014. Lecture Notes in Computer Science, vol 8702. Springer, Cham. https://doi.org/10.1007/978-3-319-10431-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-10431-7_3
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10430-0
Online ISBN: 978-3-319-10431-7
eBook Packages: Computer ScienceComputer Science (R0)