### 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.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics
- Computer science/Algorithms

### Session IMP2

- IMP2_Aux_Lemmas
- IMP2_Utils
- Named_Simpsets
- Subgoal_Focus_Some
- Syntax
- Semantics
- Annotated_Syntax
- IMP2_Basic_Simpset
- Parser
- IMP2_Basic_Decls
- IMP2_Program_Analysis
- IMP2_Var_Postprocessor
- IMP2_Var_Abs
- IMP2_VCG
- IMP2_Specification
- IMP2
- Quickstart_Guide
- IMP2_from_IMP
- Examples

### Used by

- Binary Heaps for IMP2

## Cite

×

IMP2-AFP

    @article{IMP2-AFP,
      author  = {Peter Lammich and Simon Wimmer},
      title   = {IMP2 – Simple Program Verification in Isabelle/HOL},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/IMP2.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Jan 15, 2019 : Isabelle2018