Peter Lammich

(Department of Computer Science, RPTU)
hosted by Department of Computer Science

"Stepwise Refinement for Provably Correct and Efficient Software"

Stepwise refinement in combination with interactive theorem provers is a powerful tool to verify efficient implementations of complex algorithms.
In this talk, we present the Isabelle Refinement Framework, an implementation of stepwise refinement in the Isabelle/HOL theorem prover. It can be used to verify sequential and parallel algorithms, down to their efficient implementations. We have applied it to algorithms from various areas, including SAT-solving, model-checking,graph-algorithms, and sorting. The Isabelle Refinement Framework uses LLVM as its back-end, such that the verified algorithms can be readily used in standard software toolchains.

Time:	Friday, 19.01.2024, 12:30
Place:

Termin als Datei downloaden und in den Kalender importieren.