| 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}}
|