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

@inproceedings{schirmer-04, 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}} }