A Verification Environment for Sequential Imperative Programs in Isabelle/HOL

Norbert Schirmer

Paper on the Workshop on Operating Systems Verification, October 5, 2004, Sydney, Australia


We develop a general language model for sequential imperative programs together with a Hoare logic. We instantiate the framework with common programming language constructs and integrate it into Isabelle/HOL, to gain a usable and sound verification environment.

 Online Copy

Available as PDF-File (265KB)

 BibTeX Entry

author = {Norbert Schirmer},
title = {A {V}erification {E}nvironment for {S}equential {I}mperative {P}rograms in {Isabelle/HOL}},
booktitle = {Proc. {NICTA} {W}orkshop on {OS} {V}erification 2004},
institution = {{NICTA}},
year = {2004},
editor = {Gerwin Klein},
note = {ID: 0401005T-1,  available from \url{http://www4.in.tum.de/~schirmer}}

Norbert Schirmer
Last modified: Tue Jan 11 10:27:19 MET 2005