License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2016.8
URN: urn:nbn:de:0030-drops-98562
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9856/
Go to the corresponding LIPIcs Volume Portal

Chrzaszcz, Jacek ; Schubert, Aleksy ; Zakrzewski, Jakub

Coq Support in HAHA

pdf-format:
LIPIcs-TYPES-2016-8.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{chrzaszcz_et_al:LIPIcs:2018:9856,
  author =	{Jacek Chrzaszcz and Aleksy Schubert and Jakub Zakrzewski},
  title =	{{Coq Support in HAHA}},
  booktitle =	{22nd International Conference on Types for Proofs and  Programs (TYPES 2016)},
  pages =	{8:1--8:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Silvia Ghilezan and Herman Geuvers and Jelena Ivetić},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9856},
  URN =		{urn:nbn:de:0030-drops-98562},
  doi =		{10.4230/LIPIcs.TYPES.2016.8},
  annote =	{Keywords: Hoare logic, program verification, Coq theorem prover, teaching}
}

Keywords: Hoare logic, program verification, Coq theorem prover, teaching
Collection: 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Issue Date: 2018
Date of publication: 05.11.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI