Abstract |
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 (244KB) |
BibTeX Entry |
@inproceedings{Schirmer-LPAR04, author={Norbert Schirmer}, title={A Verification Environment for Sequential Imperative Programs in {I}sabelle/{HOL}}, booktitle="Logic for Programming, Artificial Intelligence, and Reasoning", editor="F. Baader and A. Voronkov", year=2005,publisher=Springer,series=LNAI,volume=3452,pages={398--414}} |