Refinement for Monadic Programs. We provide a framework for program and data refinement in Isabelle/HOL. The framework is based on a nondeterminism-monad with assertions, i.e., the monad carries a set of results or an assertion failure. Recursion is expressed by fixed points. For convenience, we also provide while and foreach combinators. The framework provides tools to automatize canonical tasks, such as verification condition generation, finding appropriate data refinement relations, and refine an executable program to a form that is accepted by the Isabelle/HOL code generator.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Lammich, Peter: Refinement to imperative HOL (2019)
- Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
- Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
- Immler, Fabian: A verified ODE solver and the Lorenz attractor (2018)
- Lammich, Peter; Sefidgar, S. Reza: Formalizing the Edmonds-Karp algorithm (2016)
- Lammich, Peter: Verified efficient implementation of Gabow’s strongly connected component algorithm (2014)