|
IMP2
–
Simple
Program
Verification
in
Isabelle/HOL
Title: |
IMP2 – Simple Program Verification in Isabelle/HOL |
Authors:
|
Peter Lammich and
Simon Wimmer
|
Submission date: |
2019-01-15 |
Abstract: |
IMP2 is a simple imperative language together with Isabelle tooling to
create a program verification environment in Isabelle/HOL. The tools
include a C-like syntax, a verification condition generator, and
Isabelle commands for the specification of programs. The framework is
modular, i.e., it allows easy reuse of already proved programs within
larger programs. This entry comes with a quickstart guide and a large
collection of examples, spanning basic algorithms with simple proofs
to more advanced algorithms and proof techniques like data refinement.
Some highlights from the examples are: - Bisection
Square Root,
- Extended Euclid,
- Exponentiation by Squaring,
- Binary
Search,
- Insertion Sort,
- Quicksort,
- Depth First Search.
The abstract syntax and semantics are very
simple and well-documented. They are suitable to be used in a course,
as extension to the IMP language which comes with the Isabelle
distribution. While this entry is limited to a simple imperative
language, the ideas could be extended to more sophisticated languages. |
BibTeX: |
@article{IMP2-AFP,
author = {Peter Lammich and Simon Wimmer},
title = {IMP2 – Simple Program Verification in Isabelle/HOL},
journal = {Archive of Formal Proofs},
month = jan,
year = 2019,
note = {\url{http://isa-afp.org/entries/IMP2.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Used by: |
IMP2_Binary_Heap |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|