License
when quoting this document, please refer to the following
DOI: 10.4230/OASIcs.SSV.2011.1
URN: urn:nbn:de:0030-drops-35864
URL: http://drops.dagstuhl.de/opus/volltexte/2012/3586/

Gast, Holger

Structuring Interactive Correctness Proofs by Formalizing Coding Idioms

pdf-format:
Dokument 1.pdf (520 KB)


Abstract

This paper examines a novel strategy for developing correctness proofs in interactive software verification for C programs. Rather than proceeding backwards from the generated verification conditions, we start by developing a library of the employed data structures and related coding idioms. The application of that library then leads to correctness proofs that reflect informal arguments about the idioms. We apply this strategy to the low-level memory allocator of the L4 microkernel, a case study discussed in the literature.

BibTeX - Entry

@InProceedings{gast:OASIcs:2012:3586,
  author =	{Holger Gast},
  title =	{{Structuring Interactive Correctness Proofs by Formalizing Coding Idioms}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  pages =	{1--14},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{J{\"o}rg Brauer and Marco Roveri and Hendrik Tews},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3586},
  URN =		{urn:nbn:de:0030-drops-35864},
  doi =		{http://dx.doi.org/10.4230/OASIcs.SSV.2011.1},
  annote =	{Keywords: software verification, coding idioms, theory re-use, low-level code}
}

Keywords: software verification, coding idioms, theory re-use, low-level code
Seminar: 6th International Workshop on Systems Software Verification
Issue date: 2012
Date of publication: 12.07.2012


DROPS-Home | Fulltext Search | Imprint Published by LZI