[Club2] Invitation: Refinement to Imperative/HOL @ Wed Aug 12, 2015 16:00 - 17:00 (Club2)

[julianbrunner at gmail.com]

You have been invited to the following event.

Title: Refinement to Imperative/HOL
Speaker: Peter Lammich
Type: ITP Rehearsal Talk
Abstract:

Many algorithms can be implemented most efficiently with imperative data  
structures that support destructive update. In this paper we present an  
approach to automatically generate verified imperative implementations from  
abstract specifications in Isabelle/HOL. It is based on the Isabelle  
Refinement Framework, for which a lot of abstract algorithms are already  
formalized.

Based on Imperative/HOL, which allows to generate verified imperative code,  
we develop a separation logic framework with automation to make it  
conveniently usable. On top of this, we develop an imperative collection  
framework, which provides standard implementations for sets and maps like  
hash tables and array lists. Finally, we define a refinement calculus to  
refine abstract (functional) algorithms to imperative ones.

Moreover, we have implemented a tool to automate the refinement process,  
replacing abstract data types by efficient imperative implementations from  
our collection framework. As a case study, we apply our tool to  
automatically generate verified imperative implementations of nested  
depth-first search and Dijkstra's shortest paths algorithm, which are  
considerably faster than the corresponding functional implementations. The  
nested DFS implementation is almost as fast as a C++ implementation of the  
same algorithm.
When: Wed Aug 12, 2015 16:00 - 17:00 Berlin
Where: MI 00.09.038 (Turing)
Calendar: Club2
Who:
     * julianbrunner at gmail.com - creator
     * club2 at mailbroy.informatik.tu-muenchen.de

Event details:  
https://www.google.com/calendar/event?action=VIEW&eid=NzUxN2hlZnFiMWxlNTJzanE1aXBzanE0N28gY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWY3NGJkOTJkYjgxNTBmNTdkYTRjMDA5OTQwMWY0OWIxMzhmNGU2ZTA&ctz=Europe/Berlin&hl=en

Invitation from Google Calendar: https://www.google.com/calendar/

You are receiving this courtesy email at the account  
club2 at mailbroy.informatik.tu-muenchen.de because you are an attendee of  
this event.

To stop receiving future updates for this event, decline this event.  
Alternatively you can sign up for a Google account at  
https://www.google.com/calendar/ and control your notification settings for  
your entire calendar.

Forwarding this invitation could allow any recipient to modify your RSVP  
response. Learn more at  
https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20150805/41073d4b/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2477 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20150805/41073d4b/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2525 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20150805/41073d4b/attachment.bin>