A Verification Environment for Sequential Imperative Programs in Isabelle/HOL

Norbert Schirmer

Paper on the LPAR 2004 --- International Conference on Logic for Programming Artificial Intelligence and Reasoning, March 14-18, 2005, Montevideo, Uruguay


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


Norbert Schirmer
Last modified: Thu Mar 24 16:45:59 MET 2005