Document Open Access Logo

Coq Support in HAHA

Authors Jacek Chrzaszcz, Aleksy Schubert, Jakub Zakrzewski

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2016.8.pdf
  • Filesize: 0.72 MB
  • 26 pages

Document Identifiers

Author Details

Jacek Chrzaszcz
Aleksy Schubert
Jakub Zakrzewski

Cite AsGet BibTex

Jacek Chrzaszcz, Aleksy Schubert, and Jakub Zakrzewski. Coq Support in HAHA. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 8:1-8:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2016.8

Abstract

HAHA is a tool that helps in teaching and learning Hoare logic. It is targeted at an introductory course on software verification. We present a set of new features of the HAHA verification environment that exploit Coq. These features are (1) generation of verification conditions in Coq so that they can be explored and proved interactively and (2) compilation of HAHA programs into CompCert certified compilation tool-chain. With the interactive Coq proving support we obtain an interesting functionality that makes it possible to carefully examine step-by-step verification conditions and systematically discover flaws in their formulation. As a result Coq back-end serves as a kind of specification debugger.
Keywords
  • Hoare logic
  • program verification
  • Coq theorem prover
  • teaching

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Proc. of CAV 2011, volume 6806 of LNCS, pages 171-177. Springer, 2011. Google Scholar
  2. Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.4, 2009. Google Scholar
  3. Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a C compiler front-end. In FM 2006: Int. Symp. on Formal Methods, volume 4085 of LNCS, pages 460-475. Springer, 2006. URL: http://gallium.inria.fr/~xleroy/publi/cfront.pdf.
  4. A garbage collector for C and C++. Retrieved November 16, 2016, from URL: http://www.hboehm.info/gc/.
  5. Sylvie Boldo and Claude Marché. Formal verification of numerical programs: From C annotated programs to mechanical proofs. Mathematics in Computer Science, 5(4):377-393, December 2011. Google Scholar
  6. Richard Bubel and Reiner Hähnle. A Hoare-style calculus with explicit state updates. In Zoltán Instenes, editor, Proc. of Formal Methods in Computer Science Education (FORMED), ENTCS, pages 49-60. Elsevier, 2008. Google Scholar
  7. Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Proc. of FMCO 2005, pages 342-363, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  8. Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceeding of the 16th ACM SIGPLAN International Conference on Functional programming (ICFP), pages 418-430. ACM, 2011. Google Scholar
  9. Adam Chlipala. Certified Programming with Dependent Types. The MIT Press, 2013. Google Scholar
  10. David R. Cok and Joseph R. Kiniry. ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system. In Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean, editors, Proc. of CASSIS 2004, volume 3362 of LNCS, pages 108-128. Springer, 2005. Google Scholar
  11. P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the Ninthteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 83-94, Albuquerque, New Mexico, January 1992. ACM Press, New York, NY. Google Scholar
  12. Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C - A software analysis perspective. In George Eleftherakis, Mike Hinchey, and Mike Holcombe, editors, Proc. of SEFM'12, volume 7504 of LNCS. Springer, 2012. Google Scholar
  13. Markus Dahlweid, Michal Moskal, Thomas Santen, Stephan Tobies, and Wolfram Schulte. VCC: Contract-based modular verification of concurrent C. In ICSE Companion, pages 429-430. IEEE, 2009. Google Scholar
  14. Zaynah Dargaye. Vérification formelle d'un compilateur pour langages fonctionnels. PhD thesis, Université Paris 7 Diderot, July 2009. Google Scholar
  15. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proc. of TACAS'08, volume 4963 of LNCS, pages 337-340. Springer, 2008. Google Scholar
  16. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Proc. of ESOP'13, volume 7792 of LNCS, pages 125-128. Springer, 2013. Google Scholar
  17. Google Java style guide. Retrieved November 16, 2016, from URL: https://google.github.io/styleguide/javaguide.html.
  18. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. Google Scholar
  19. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and Java. In Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods, volume 6617 of LNCS, pages 41-55. Springer, 2011. Google Scholar
  20. K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC/Java user’s manual. Technical note, Compaq Systems Research Center, October 2000. Google Scholar
  21. Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In Proc. of POPL'2006, pages 42-54. ACM Press, 2006. URL: http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf.
  22. Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363-446, 2009. Google Scholar
  23. Xavier Leroy. Mechanized semantics for compiler verification. In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems, 10th Asian Symposium, APLAS 2012, volume 7705 of LNCS, pages 386-388. Springer, 2012. Abstract of invited talk. URL: http://gallium.inria.fr/~xleroy/publi/mechanized-semantics-aplas-cpp-2012.pdf.
  24. Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Information and Computation, 207(2):284-304, 2009. URL: http://gallium.inria.fr/~xleroy/publi/coindsem-journal.pdf.
  25. Linux kernel coding style. Retrieved November 16, 2016, from URL: https://www.kernel.org/doc/Documentation/CodingStyle.
  26. Tadeusz Sznuk and Aleksy Schubert. Tool support for teaching Hoare logic. In Dimitra Giannakopoulou and Gwen Salaün, editors, Proc. of SEFM 2014, volume 8702 of LNCS, pages 332-346. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-10431-7_27.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact