Abstract
This paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are mapped to higher-level data types for verification. The programming language is embedded in higher-order logic, its Hoare logic is derived. The whole development is purely definitional and thus sound. The viability of this approach is demonstrated with a non-trivial case study. We show the correctness of the Schorr-Waite graph marking algorithm and present part of the readable proof in Isabelle/HOL.
This is a preview of subscription content, log in via an institution to check access.
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
Bornat, R.: Proofs of pointer programs in Jape, http://www.dcs.qmul.ac.uk/~richard/pointers/
Bornat, R.: Proving pointer programs in Hoare Logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000)
Bornat, R., Sufrin, B.: Animating formal proofs at the surface: the Jape proof calculator. The Computer Journal 43, 177–192 (1999)
Burstall, R.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 7, pp. 23–50. Edinburgh University Press (1972)
Gordon, M.C.J.: Mechanizing programming logics in higher order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automated Theorem Proving. Springer, Heidelberg (1989)
Jensen, J.L., Joergensen, M.E., Klarlund, N., Schwartzbach, M.I.: Automatic verification of pointer programs using monadic secondorder logic. In: PLDI 1997 (1997)
Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic, http://www.in.tum.de/~nipkow/pubs/cade03.html
Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing 10, 171–186 (1998)
Nipkow, T.: Structured Proofs in Isar/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 259–278. Springer, Heidelberg (2003)
Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of Lect. Notes in Comp. Sci. Springer-Verlag, 2002. http://www.in.tum.de/~nipkow/LNCS2283/.
Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structures. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millenial Perspectives in Computer Science, Houndsmill, Hampshire, pp. 303–321. Palgrave, Oxford (2000)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55–74 (2002)
Suzuki, N.: Automatic Verification of Programs with Complex Data Structures. PhD thesis, Stanford University (1976); Garland Publishing (1980)
Wenzel, M.: Isabelle/Isar — A Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Institut für Informatik, Technische Universität München (2002), http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html
Yang, H.: Local Reasoning for Stateful Programs. PhD thesis, University of Illinois, Urbana-Champaign (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mehta, F., Nipkow, T. (2003). Proving Pointer Programs in Higher-Order Logic. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-45085-6_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40559-7
Online ISBN: 978-3-540-45085-6
eBook Packages: Springer Book Archive