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

Dmitriy Traytel traytel at in.tum.de
Tue Jul 16 13:59:15 CEST 2013


Am 11.07.2013 15:50, schrieb Andrei Popescu:
> Correction: The two afternoon talks start at 16:30 and end at 17:30 
> (half an hour shift from the original announcement).
>
> 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 
> Haslbeckin the afternoon.
>
> Cheers,
>    Andrei
>
> First talk:
>
> Yutaka Nagashima
> Data Parallel Algorithms in Haskell and their Verification in Isabelle/HOL
> ==========================================================================
> Tue. July 16, 16:30, 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, 17:00, 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.
>
>
>
>
> _______________________________________________
> Club2 mailing list
> List page: https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/club2
> Webpage with calendar: http://www21.in.tum.de/club2

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130716/9f41135e/attachment.html>


More information about the Club2 mailing list