[Club2] Invitation: Verification of the Decrease-Key Operation in Fibonacci H... @ Wed Jun 3, 2020 14:35 - 15:10 (CEST) (club2 at mailbroy.informatik.tu-muenchen.de)

[julianbrunner at gmail.com]

You have been invited to the following event.

Title: Verification of the Decrease-Key Operation in Fibonacci Heaps in  
Imperative-HOL

Speaker: Simon Griebel
Type: Master's Thesis Presentation
Abstract:In this thesis, we present a proof of the functional correctness  
of the Fibonacci heap decrease-key operation using a separation logic  
framework implemented for Imperative-HOL, an imperative verification  
framework built on top of Isabelle/HOL. This is a follow-up on Daniel  
Stüwe’s Master’s thesis, where he verified all Fibonacci heap operations  
(most notably delete-min) except for decrease-key and delete, which require  
a handle to the element to be changed or removed, respectively. His  
approach is based on first verifying a functional version of the Fibonacci  
heap and then showing that the imperative implementation correctly models  
the functional one. Using an augmented version of his approach, which also  
works for decrease-key, turned out to be too complex. Thus, the  
decrease-key operation was proven with an alternative approach where the  
heap is modeled as a map from addresses to (abstract) heap nodes.
Together with Daniel Stüwe’s thesis, this means that the complete  
functionality of the Fibonacci heap was verified, even though the two  
different approaches are not directly compatible. For that reason, we also  
proved the functional correctness of make-heap, heap-union, get-min, and of  
a function creating a heap with a single element with the help of the new  
approach.
When: Wed Jun 3, 2020 14:35 – 15:10 Central European Time - Berlin
Where: https://bbb.rbg.tum.de/kev-tnx-732
Calendar: club2 at mailbroy.informatik.tu-muenchen.de
Who:
     * julianbrunner at gmail.com - creator
     * club2 at mailbroy.informatik.tu-muenchen.de
     * s.griebel at tum.de

Event details:  
https://www.google.com/calendar/event?action=VIEW&eid=NXBkN2h2bG9xMW5yMHVoNThxbGUzZnVyYWsgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWM4MTVhNDhjOTE0YmE4MjVlMzg0ODQyN2Q4MTFmZTlkYWZlYjdhNjI&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/20200519/1018be61/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 3116 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20200519/1018be61/attachment-0001.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 3173 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20200519/1018be61/attachment-0001.bin>