See Group colloquium

The Isabelle Refinement Framework by Peter Lammich, Assistant Professor University of Twente

Abstract: In this talk, we give an overview of the Isabelle Refinement Framework, a framework to verify software with the interactive theorem prover Isabelle/HOL, using a stepwise refinement approach. It's combination of stepwise refinement to structure the proof, powerful automation for canonical but tedious proofs, and interactive proving for the complicated parts of the proof allow for the verification of complex algorithms and software.