[Club2] Talk by Manuel Eberl, Wed. Oct. 24, 10:00, Alonzo Church

[Andrei Popescu]

Dear All,  
The coming Wednesday, we will have a bachelor thesis talk by Manuel Eberl on the Isabelle verification and code generation for a simulation relation algorithm.  
Best regards,   Andrei 
Manuel Eberl  (Bachelor thesis)====================================================Wed. Oct.
 24, 10:00, MI 01.09.014 ("Alonzo Church")  
We implemented the algorithm by Ilie, Navarro, and Yu for computingsimulation relations on Nondeterministic Finite Automata and verified itwith Isabelle using Peter Lammich’s Monadic Refinement Framework: anabstract version of the algorithm was formalised, proven correct, andthen refined by successively replacing parts of it with more concretecommands until executable code was obtained. This code was then exportedto ML and evaluated with regard to performance compared to unverified,imperative
 code.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20121017/55c586b7/attachment.html>