Email Gateway (Aug 22 2022 at 18:56): Email Gateway (Aug 22 2022 at 18:56):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to announce a new AFP-entry. It contains tools to specify and verify imperative programs in Isabelle/HOL, as well as several examples.
IMP2 – Simple Program Verification in Isabelle/HOL
by Peter Lammich and Simon Wimmer
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:
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.
For more details, have a look at https://www.isa-afp.org/entries/IMP2.html
Enjoy,
René
Last updated: Apr 24 2024 at 20:16 UTC