Arthur Charguéraud
ABSTRACT
In previous work, we introduced an approach to program verification based on characteristic formulae. The approach consists of generating a higher-order logic formula from the source code of a program. This characteristic formula is constructed in such a way that it gives a sound and complete description of the semantics of that program. The formula can thus be exploited in an interactive proof assistant to formally verify that the program satisfies a particular specification.
This previous work was, however, only concerned with purely-functional programs. In the present paper, we describe the generalization of characteristic formulae to an imperative programming language. In this setting, characteristic formulae involve specifications expressed in the style of Separation Logic. They also integrate the frame rule, which enables local reasoning. We have implemented a tool based on characteristic formulae. This tool, called CFML, supports the verification of imperative Caml programs using the Coq proof assistant. Using CFML, we have formally verified nontrivial imperative algorithms, as well as CPS functions, higher-order iterators, and programs involving higher-order stores.
Supplemental Material
- Andrew W. Appel. Tactics for separation logic. Unpublished draft, http://www.cs.princeton.edu/appel/papers/septacs.pdf, 2006.Google Scholar
- Mike Barnett, Rob DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6), 2004.Google ScholarCross Ref
- Bruno Barras and Bruno Bernardo. The implicit calculus of constructions as a programming language with dependent types. In FoSSaCS, volume 4962 of LNCS, pages 365--379. Springer, 2008. Google ScholarDigital Library
- Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt. Verification of Object-Oriented Software: The KeY Approach, volume 4334 of LNCS. Springer-Verlag, Berlin, 2007. Google ScholarDigital Library
- Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In International Symposium on Formal Methods for Components and Objects, volume 4111 of LNCS, pages 115--137. Springer, 2005. Google ScholarDigital Library
- Martin Berger, Kohei Honda, and Nobuko Yoshida. A logical analysis of aliasing in imperative higher-order functions. In ICFP, pages 280--293, 2005. Google ScholarDigital Library
- Arthur Charguéraud. Verification of call-by-value functional programs through a deep embedding. 2009. Unpublished. http://arthur.chargueraud.org/research/2009/deep/.Google Scholar
- Arthur Charguéraud. Characteristic Formulae for Mechanized Program Verification. PhD thesis, Université Paris-Diderot, 2010.Google Scholar
- Arthur Charguéraud. Program verification through characteristic formulae. In ICFP, pages 321--332. ACM, 2010. Google ScholarDigital Library
- Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. Effective interactive proofs for higher-order imperative programs. In ICFP, 2009. Google ScholarDigital Library
- The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 8.2, 2009.Google Scholar
- Jean-Christophe Filliâtre. Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709--745, 2003. Google ScholarDigital Library
- Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In PLDI, pages 237--247, 1993. Google ScholarDigital Library
- Susanne Graf and Joseph Sifakis. A modal characterization of observational congruence on finite terms of CCS. Information and Control, 68(1-3):125--145, 1986. Google ScholarDigital Library
- David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. The MIT Press, Cambridge, Massachusetts, 2000. Google ScholarCross Ref
- Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In ICALP, volume 85 of LNCS, pages 299--309. Springer-Verlag, 1980. Google ScholarDigital Library
- C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--580, 583, 1969. Google ScholarDigital Library
- Kohei Honda, Martin Berger, and Nobuko Yoshida. Descriptive and relative completeness of logics for higher-order functions. In ICALP, volume 4052 of LNCS. Springer, 2006. Google ScholarDigital Library
- Bart Jacobs and Erik Poll. Java program verification at nijmegen: Developments and perspective. In ISSS, volume 3233 of LNCS, pages 134--153. Springer, 2003.Google Scholar
- Johannes Kanig and Jean-Christophe Filliâtre. Who: a verifier for effectful higher-order programs. In ML'09: Proceedings of the 2009 ACM SIGPLAN workshop on ML, pages 39--48. ACM, 2009. Google ScholarDigital Library
- Gerwin Klein, Philip Derrin, and Kevin Elphinstone. Experience report: seL4: formally verifying a high-performance microkernel. In ICFP, pages 91--96. ACM, 2009. Google ScholarDigital Library
- Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd Symposium on Operating Systems Principles (SOSP), Operating Systems Review (OSR), pages 207--220, Big Sky, MT, 2009. ACM SIGOPS. Google ScholarDigital Library
- Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL, pages 42--54, 2006. Google ScholarDigital Library
- Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The Objective Caml system, 2005.Google Scholar
- Pierre Letouzey. Programmation fonctionnelle certifiée - l'extraction de programmes dans l'assistant Coq. PhD thesis, Université Paris 11, 2004.Google Scholar
- Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa. Towards formal verification of memory properties using separation logic, 2005.Google Scholar
- Andrew McCreight. Practical tactics for separation logic. In TPHOLs, volume 5674 of LNCS, pages 343--358. Springer, 2009. Google ScholarDigital Library
- Farhad Mehta and Tobias Nipkow. Proving pointer programs in higher-order logic. Information and Computation, 199(1-2), 2005. Google ScholarDigital Library
- Magnus O. Myreen. Formal Verification of Machine-Code Programs. PhD thesis, University of Cambridge, 2008.Google Scholar
- Magnus O. Myreen. Separation logic adapted for proofs by rewriting. In Interactive Theorem Proving (ITP), volume 6172 of LNCS, pages 485--489. Springer, 2010. Google ScholarDigital Library
- Magnus O. Myreen and Michael J. C. Gordon. Verified LISP implementations on ARM, x86 and powerPC. In TPHOLs, volume 5674 of LNCS, pages 359--374. Springer, 2009. Google ScholarDigital Library
- Aleksandar Nanevski and Greg Morrisett. Dependent type theory of stateful higher-order functions. Technical Report TR-24-05, Harvard University, 2005.Google Scholar
- Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. Journal of Functional Programming, 18(5--6):865--911, 2008. Google ScholarDigital Library
- Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. Structuring the verification of heap-manipulating programs. In POPL, pages 261--274. ACM, 2010. Google ScholarDigital Library
- Zhaozhong Ni and Zhong Shao. Certified assembly programming with embedded code pointers. In POPL, 2006. Google ScholarDigital Library
- Peter O'Hearn, John Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In CSL, volume 2142 of LNCS, pages 1--19, Berlin, 2001. Springer-Verlag. Google ScholarDigital Library
- Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1999. Google ScholarDigital Library
- Yann Régis-Gianas and François Pottier. A Hoare logic for call-by-value functional programs. In MPC, 2008. Google ScholarDigital Library
- John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55--74, 2002. Google ScholarDigital Library
- Hayo Thielecke. Frame rules from answer types for code pointers. In POPL, pages 309--319, 2006. Google ScholarDigital Library
- Thomas Tuerk. Local reasoning about while-loops. In VSTTE LNCS, 2010.Google Scholar
- Karen Zee, Viktor Kuncak, and Martin C. Rinard. An integrated proof language for imperative programs. In PLDI, pages 338--351. ACM, 2009. Google ScholarDigital Library
Index Terms
- Characteristic formulae for the verification of imperative programs
Recommendations
Program verification through characteristic formulae
ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programmingThis paper describes CFML, the first program verification tool based on characteristic formulae. Given the source code of a pure Caml program, this tool generates a logical formula that implies any valid post-condition for that program. One can then ...
Characteristic formulae for the verification of imperative programs
ICFP '11In previous work, we introduced an approach to program verification based on characteristic formulae. The approach consists of generating a higher-order logic formula from the source code of a program. This characteristic formula is constructed in such ...
Program verification through characteristic formulae
ICFP '10This paper describes CFML, the first program verification tool based on characteristic formulae. Given the source code of a pure Caml program, this tool generates a logical formula that implies any valid post-condition for that program. One can then ...
Comments