[Club2] talks by Yutaka Nagashima and Maximilian Haslbeck, Tue. July 16, 16:00, Turing

[Andrei Popescu]

Dear All, 

Tuesday July 16 is a very busy listening day.  Besides Peter's talk in the morning, we also have two 
Master's thesis presentations by Yutaka Nagashima and Maximilian Haslbeck in the afternoon.

Cheers, 
   Andrei

First talk:

Yutaka Nagashima
Data Parallel Algorithms in Haskell and their Verification in Isabelle/HOL
==========================================================================
Tue. July 16, 16:00, Alan Turing  

Ever-faster computational power is required in many fields, and
parallel computer architectures are commonly used to obtain better
performance. Data parallelism is one approach to achieve performance
gains using multi-core architectures.

The aim of this project is to verify data parallel algorithms in
Isabelle/HOL and to create Data Parallel Haskell (DPH) modules from
verified executable definitions using Isabelle's code generator. The
serialiser of the code generator is extended with a facility to
generate DPH code. Case studies have been carried out to demonstrate
our approach. A generated verified DPH module shows a speed-up by
exploiting the multi-core architecture.

Second talk:

Maximilian Haslbeck
Verified decision procedures for the equivalence of regular expressions
=========================================================
Tue. July 16, 16:30, Alan Turing 

Many procedures for deciding regular expression equivalence were proposed. We formalize and verify
four executable methods that do not need automata but work directly on regular expressions: based on
derivatives, partial derivatives and two closely related versions of pointed regular expressions.
The methods can be formulated in a generic algorithm, for which we show soundness, termination and completeness.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130711/a53255f2/attachment-0001.html>