[Club2] Invitation: Verification of Fibonacci Heaps in Imperative HOL @ Wed May 15, 2019 16:30 - 17:15 (CEST) (club2 at mailbroy.informatik.tu-muenchen.de)

[julianbrunner at gmail.com]

You have been invited to the following event.

Title: Verification of Fibonacci Heaps in Imperative HOL
Speaker: Daniel Stüwe
Type: Master's Thesis Presentation
Abstract:
Fibonacci heaps are one of the most important implementations of priority  
queues since their discovery led to a lowered worst-case runtime of certain  
greedy algorithms, e g. Dijskstra’s or Prim’s algorithm. The necessary  
proofs employ an amortized runtime analysis. Apart from this, they are  
considered in general to be one of the more complex data structures.  
Therefore, we formally verify Fibonacci heaps in this thesis. Our approach  
is to define and prove correct a functional implementation first, which is  
then refined to an imperative version. To our knowledge, this is the first  
formal verification of Fibonacci Heaps including functional correctness,  
imperative implementation and amortized runtime for the all operations  
except for decrease-key.
When: Wed May 15, 2019 16:30 – 17:15 Central European Time - Berlin
Where: MI 00.05.055
Calendar: club2 at mailbroy.informatik.tu-muenchen.de
Who:
     * julianbrunner at gmail.com - creator
     * lammich at in.tum.de
     * stuewe at in.tum.de
     * club2 at mailbroy.informatik.tu-muenchen.de
     * jiangn at in.tum.de
     * aplatzer at andrew.cmu.edu

Event details:  
https://www.google.com/calendar/event?action=VIEW&eid=Nm90Y2hzczNuaWxsYnN0dmo5NzNoMWRqZmIgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTIyNTNhZGYwOGI2NTEyZmQ5NjYxNDFiOGYyNGYxNjAzMDJhYzYwODA&ctz=Europe%2FBerlin&hl=en&es=0

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 send a response to  
the organizer and be added to the guest list, or invite others regardless  
of their own invitation status, or to modify your RSVP. Learn more at  
https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20190508/fa2dfab2/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2777 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20190508/fa2dfab2/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2829 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20190508/fa2dfab2/attachment.bin>