Reasoning about Partial Correctness Assertions in Isabelle/HOL

Authors

DOI:

https://doi.org/10.22456/2175-2745.98483

Keywords:

Hoare Logic, program verification, theorem proving

Abstract

Hoare Logic has a long tradition in formal verification and has been continuously developed and used to verify a broad class of programs, including sequential, object-oriented and concurrent programs. The purpose of this work is to provide a detailed and accessible exposition of the several ways the user can conduct, explore and write proofs of correctness of sequential imperative programs with Hoare logic and the ISABELLE proof assistant. With the proof language Isar, it is possible to write structured, readable proofs that are suitable for human understanding and communication.

Downloads

Download data is not yet available.

Author Biography

Alfio Ricardo Martini, Av. Marechal Andrea 11/210, Porto Alegre/RS/Brasil

Computer Scientist, passionate about programming, formal reasoning and education, with a strong basis in discrete mathematics, logic, data structures, category theory, formal verification and functional programming. Especially interested in the relations and applications of functional programming techniques in the area of Web Programming

References

FLOYD, R. W. Assigning meanings to programs. Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, v. 19, 01 1967.

HOARE, C. A. R. An axiomatic basis for computer programming. Commun. ACM, v. 12, n. 10, p. 576–580, 1969.

APT, K. R.; BOER, F. de; OLDEROG, E.-R. Verification of Sequential and Concurrent Programs. 3rd. ed. [S.l.]: Springer Publishing Company, Incorporated, 2009.

ANDREWS, G. R. Concurrent Programming: Principles and Practice. Redwood City, CA, USA: Benjamin-Cummings Publishing Co., Inc., 1991.

NIPKOW, T.; WENZEL, M.; PAULSON, L. C. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Berlin, Heidelberg: Springer-Verlag, 2002.

APPEL, A. W. et al. Program Logics for Certified Compilers. New York, NY, USA: Cambridge University Press, 2014.

BERTOT, Y.; CASTRAN, P. Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions. 1st. ed. [S.l.]: Springer Publishing Company, Incorporated, 2010.

FILLI TRE, J.-C. One Logic To Use Them All. In: BONACINA, M. P. (Ed.). CADE 24 - the 24th International Conference on Automated Deduction. Lake Placid, NY, United States: Springer, 2013.

LEINO, R. Dafny: An automatic program verifier for functional correctness. In: 16th International Conference, LPAR-16, Dakar, Senegal. [S.l.]: Springer Berlin Heidelberg, 2010. p. 348–370.

BUBEL, R.; HÄHNLE, R. Key-hoare. In: Deductive Software Verification - The KeY Book - From Theory to Practice. [S.l.: s.n.], 2016. p. 571–589.

WINSKEL, G. The Formal Semantics of Programming Languages - an Introduction. [S.l.]: MIT Press, 1993. I-XVIII, 1-361 p. (Foundation of computing series).

HEIN, J. Discrete Structures, Logic, and Computability. [S.l.]: Jones & Bartlett Learning, 2010.

NIELSON, H. R.; NIELSON, F. Semantics with Applications - a Formal Introduction. [S.l.]: Wiley, 1992. I-XII, 1-240 p. (Wiley professional computing).

BRADLEY, A. R.; MANNA, Z. The Calculus of Computation: Decision Procedures with Applications to Verification. Berlin, Heidelberg: Springer-Verlag, 2007.

LOECKX, J.; SIEBER, K.; STANSIFER, R. D. The Foundations of Program Verification. New York, NY, USA: John Wiley & Sons, Inc., 1984.

GORDON, M. J. C. Programming language theory and its implementation - applicative and imperative paradigms. [S.l.]: Prentice Hall, 1988. (Prentice Hall International series in Computer Science).

NIPKOW, T.; KLEIN, G. Concrete Semantics: With Isabelle/HOL. [S.l.]: Springer Publishing Company, Incorporated, 2014.

PAULSON, L. C. ML for the working programmer (2. ed.). [S.l.]: Cambridge University Press, 1996.

O’SULLIVAN, B.; GOERZEN, J.; STEWART, D. Real world Haskell - code you can believe in. O’Reilly, 2008. Disponível em: http://book.realworldhaskell.org/.

HAFTMANN, F. Haskell-style type classes with Isabelle/Isar. 2019. http://isabelle.in.tum.de/documentation.html.

BLANCHETE, J. User’s Guide to Sledgehammer. 2018. http://isabelle.in.tum.de/documentation.html.

SCHULZ, S.; CRUANES, S.; VUKMIROVIC, P. Faster, higher, stronger: E 2.3. In: Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. [s.n.], 2019. p. 495–507. Disponível em: https://doi.org/10.1007/978-3-030-29436-6_29.

WEIDENBACH, C. et al. Spass version 3.5. In: SCHMIDT, R. A. (Ed.). CADE. [S.l.]: Springer, 2009. (Lecture Notes in Computer Science, v. 5663), p. 140–145.

KOVÁCS, L.; VORONKOV, A. First-order theorem proving and vampire. In: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044. New York, NY, USA: Springer-Verlag New York, Inc., 2013. (CAV 2013), p. 1–35.

MOURA, L. D.; BJØRNER, N. Z3: An Efficient SMT Solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. [S.l.]: Springer-Verlag, 2008. (TACAS’08/ETAPS’08), p. 337–340.

BARRETT, C. et al. CVC4. In: GOPALAKRISHNAN, G.; QADEER, S. (Ed.). Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11). [S.l.]: Springer, 2011. (Lecture Notes in Computer Science, v. 6806), p. 171–177.

PIERCE, B. C. et al. Logical Foundations. [S.l.]: Electronic textbook, 2018. https://softwarefoundations.cis.upenn.edu/. (Software Foundations series, volume 1).

PIERCE, B. C. et al. Programming Language Foundations. [S.l.]: Electronic textbook, 2018. https://softwarefoundations.cis.upenn.edu/. (Software Foundations series, volume 2).

LEINO, K. R. M. This is boogie 2. 2008. Disponível em: https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/.

Downloads

Published

2020-06-18

How to Cite

Martini, A. R. (2020). Reasoning about Partial Correctness Assertions in Isabelle/HOL. Revista De Informática Teórica E Aplicada, 27(3), 84–101. https://doi.org/10.22456/2175-2745.98483

Issue

Section

Selected Papers - WEIT 2019