[Club2] Wed. Oct 20, 15:15: Fabian Immler

[Alexander Krauss]

Dear all,

Next Wednesday we will have a longer Club2-Session. Before Christoph 
Stoiber's talk (already announced), we will hear Fabian Immler, who 
talks about his Bachelor project.


Connecting Isabelle and SPARK
=====================================================
Wed. Oct 20, 15:15, MI 00.09.055 ("Alan Turing")


Abstract:
In the context of my Bachelors-thesis an integration of Isabelle and
the static-analysis toolset of SPARK was implemented. As a case study,
a functional specification of the cryptographic hash-algorithm
RIPEMD-160 in Isabelle/HOL was made and an implementation in the
imperative language SPARK was verified against it.