[Club2] Talk by Peter Lammich, Wed. 22, 2 PM, Turing room

[Andrei Popescu]

Dear All,  
The coming week, Peter will give a talk on his refinement framework.   
Best regards,   Andrei 
 Peter Lammich Refinement Framework for Monadic Programs in Isabelle/HOL====================================================Wed. Feb. 22, 14:00, MI 00.09.055 ("Alan Turing")
When verifying algorithms, there is a trade-off between anabstract version of the algorithm, that has a nice correctness proof butis not (or not efficiently) executable, and an implementation version,that is optimized for efficiency, but has a correctness proof that tendsto get obfuscated by implementation details.
Refinement is a top-down solution to this problem, first defining andproving correct the abstract algorithm, and then refining it (inpossibly many steps) to the concrete version, showing that eachrefinement step preserves correctness.
In this talk, we will present a refinement framework in Isabelle/HOL. Itis based on a refinement calculus for monadic expressions and providestools to automate canonical tasks such as verification conditiongeneration. The Isabelle/HOL code generator can be used to generateefficient code.
After introducing the semantic foundations of our framework, we willshow some example program development.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20120216/2567f914/attachment.html>