DROPS

Document

DOI: 10.4230/OASIcs.SSV.2011.1

Structuring Interactive Correctness Proofs by Formalizing Coding Idioms

Authors: Holger Gast

Published in: OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012)

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.

Cite as

Holger Gast. Structuring Interactive Correctness Proofs by Formalizing Coding Idioms. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{gast:OASIcs.SSV.2011.1,
  author =	{Gast, Holger},
  title =	{{Structuring Interactive Correctness Proofs by Formalizing Coding Idioms}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  pages =	{1--14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.1},
  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}
}

Search Results

Documents authored by Gast, Holger

Structuring Interactive Correctness Proofs by Formalizing Coding Idioms

Abstract

Cite as

Thanks for your feedback!

Could not send message