Department of Computer Science

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 iCAL Datei downloaden und in den Kalender importieren.






Superordinated page:

Jahr 2024

38 Vorträge

Feedback for this Page

Email to the person in charge of this page (sakdapol@informatik.uni-kl.de)