License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
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://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3586/
Go to the corresponding OASIcs Volume Portal

Gast, Holger

Structuring Interactive Correctness Proofs by Formalizing Coding Idioms

pdf-format:
2.pdf (0.5 MB)

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 =		{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
Collection: 6th International Workshop on Systems Software Verification
Issue Date: 2012
Date of publication: 13.07.2012

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