Skip to main content
Conference Proceedings

A verification environment for sequential imperative programs in isabelle/HOL

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2005) 3452 LNAI 398-414
DOI: 10.1007/978-3-540-32275-7_26
38Citations
Citations of this article
13Readers
Mendeley users who have this article in their library.
Get full text

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. © Springer-Verlag Berlin Heidelberg 2005.

Cite

CITATION STYLE

APA

Schirmer, N. (2005). A verification environment for sequential imperative programs in isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3452 LNAI, pp. 398–414). Springer Verlag. https://doi.org/10.1007/978-3-540-32275-7_26

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free