<span itemscope itemtype="http://schema.org/InformAction"><span style="display:none" itemprop="about" itemscope itemtype="http://schema.org/Person"><meta itemprop="description" content="Invitation from julianbrunner@gmail.com"/></span><span itemprop="object" itemscope itemtype="http://schema.org/Event"><div style=""><table cellspacing="0" cellpadding="8" border="0" summary="" style="width:100%;font-family:Arial,Sans-serif;border:1px Solid #ccc;border-width:1px 2px 2px 1px;background-color:#fff;"><tr><td><meta itemprop="eventStatus" content="http://schema.org/EventScheduled"/><h4 style="padding:6px 0;margin:0 0 4px 0;font-family:Arial,Sans-serif;font-size:13px;line-height:1.4;border:1px Solid #fff;background:#fff;color:#090;font-weight:normal"><strong>You have been invited to the following event.</strong></h4><div style="padding:2px"><span itemprop="publisher" itemscope itemtype="http://schema.org/Organization"><meta itemprop="name" content="Google Calendar"/></span><meta itemprop="eventId/googleCalendar" content="5pd7hvloq1nr0uh58qle3furak"/><h3 style="padding:0 0 6px 0;margin:0;font-family:Arial,Sans-serif;font-size:16px;font-weight:bold;color:#222"><span itemprop="name">Verification of the Decrease-Key Operation in Fibonacci Heaps in Imperative-HOL</span></h3><table style="display:inline-table" cellpadding="0" cellspacing="0" border="0" summary="Event details"><tr><td style="padding:0 1em 10px 0;font-family:Arial,Sans-serif;font-size:13px;color:#888;white-space:nowrap;width:90px" valign="top"><div><i style="font-style:normal">When</i></div></td><td style="padding-bottom:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222" valign="top"><div style="text-indent:-1px"><time itemprop="startDate" datetime="20200603T123500Z"></time><time itemprop="endDate" datetime="20200603T131000Z"></time>Wed Jun 3, 2020 14:35 – 15:10 <span style="color:#888">Central European Time - Berlin</span></div></td></tr><tr><td style="padding:0 1em 10px 0;font-family:Arial,Sans-serif;font-size:13px;color:#888;white-space:nowrap;width:90px" valign="top"><div><i style="font-style:normal">Where</i></div></td><td style="padding-bottom:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222" valign="top"><div style="text-indent:-1px"><span itemprop="location" itemscope itemtype="http://schema.org/Place"><span itemprop="name" class="notranslate">https://bbb.rbg.tum.de/kev-tnx-732</span><span dir="ltr"> (<a href="https://www.google.com/url?q=https%3A%2F%2Fbbb.rbg.tum.de%2Fkev-tnx-732&sa=D&ust=1590310862479000&usg=AOvVaw0XLKHL_2nnsD9Qzu1L5s1r" style="color:#20c;white-space:nowrap" target="_blank" itemprop="map">map</a>)</span></span></div></td></tr><tr><td style="padding:0 1em 10px 0;font-family:Arial,Sans-serif;font-size:13px;color:#888;white-space:nowrap;width:90px" valign="top"><div><i style="font-style:normal">Calendar</i></div></td><td style="padding-bottom:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222" valign="top"><div style="text-indent:-1px">club2@mailbroy.informatik.tu-muenchen.de</div></td></tr><tr><td style="padding:0 1em 10px 0;font-family:Arial,Sans-serif;font-size:13px;color:#888;white-space:nowrap;width:90px" valign="top"><div><i style="font-style:normal">Who</i></div></td><td style="padding-bottom:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222" valign="top"><table cellspacing="0" cellpadding="0"><tr><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222;width:10px"><div style="text-indent:-1px"><span style="font-family:Courier New,monospace">&#x2022;</span></div></td><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222"><div style="text-indent:-1px"><div><div style="margin:0 0 0.3em 0"><span itemprop="attendee" itemscope itemtype="http://schema.org/Person"><span itemprop="name" class="notranslate">julianbrunner@gmail.com</span><meta itemprop="email" content="julianbrunner@gmail.com"/></span><span style="font-size:11px;color:#888"> - creator</span></div></div></div></td></tr><tr><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222;width:10px"><div style="text-indent:-1px"><span style="font-family:Courier New,monospace">&#x2022;</span></div></td><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222"><div style="text-indent:-1px"><div><div style="margin:0 0 0.3em 0"><span itemprop="attendee" itemscope itemtype="http://schema.org/Person"><span itemprop="name" class="notranslate">club2@mailbroy.informatik.tu-muenchen.de</span><meta itemprop="email" content="club2@mailbroy.informatik.tu-muenchen.de"/></span></div></div></div></td></tr><tr><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222;width:10px"><div style="text-indent:-1px"><span style="font-family:Courier New,monospace">&#x2022;</span></div></td><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222"><div style="text-indent:-1px"><div><div style="margin:0 0 0.3em 0"><span itemprop="attendee" itemscope itemtype="http://schema.org/Person"><span itemprop="name" class="notranslate">s.griebel@tum.de</span><meta itemprop="email" content="s.griebel@tum.de"/></span></div></div></div></td></tr></table></td></tr></table><div style="float:right;font-weight:bold;font-size:13px"> <a href="https://www.google.com/calendar/event?action=VIEW&eid=NXBkN2h2bG9xMW5yMHVoNThxbGUzZnVyYWsgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWM4MTVhNDhjOTE0YmE4MjVlMzg0ODQyN2Q4MTFmZTlkYWZlYjdhNjI&ctz=Europe%2FBerlin&hl=en&es=0" style="color:#20c;white-space:nowrap" itemprop="url">more details »</a><br></div><div style="padding-bottom:15px;font-family:Arial,Sans-serif;font-size:13px;color:#222;white-space:pre-wrap!important;white-space:-moz-pre-wrap!important;white-space:-pre-wrap!important;white-space:-o-pre-wrap!important;white-space:pre;word-wrap:break-word"><span><br>Speaker: Simon Griebel<br>Type: Master's Thesis Presentation<br>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.<br>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.</span><meta itemprop="description" content="
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."/></div></div><p style="color:#222;font-size:13px;margin:0"><span style="color:#888">Going (club2@mailbroy.informatik.tu-muenchen.de)?   </span><wbr><strong><span itemprop="potentialaction" itemscope itemtype="http://schema.org/RsvpAction"><meta itemprop="attendance" content="http://schema.org/RsvpAttendance/Yes"/><span itemprop="handler" itemscope itemtype="http://schema.org/HttpActionHandler"><link itemprop="method" href="http://schema.org/HttpRequestMethod/GET"/><a href="https://www.google.com/calendar/event?action=RESPOND&eid=NXBkN2h2bG9xMW5yMHVoNThxbGUzZnVyYWsgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&rst=1&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWM4MTVhNDhjOTE0YmE4MjVlMzg0ODQyN2Q4MTFmZTlkYWZlYjdhNjI&ctz=Europe%2FBerlin&hl=en&es=0" style="color:#20c;white-space:nowrap" itemprop="url">Yes</a></span></span><span style="margin:0 0.4em;font-weight:normal"> - </span><span itemprop="potentialaction" itemscope itemtype="http://schema.org/RsvpAction"><meta itemprop="attendance" content="http://schema.org/RsvpAttendance/Maybe"/><span itemprop="handler" itemscope itemtype="http://schema.org/HttpActionHandler"><link itemprop="method" href="http://schema.org/HttpRequestMethod/GET"/><a href="https://www.google.com/calendar/event?action=RESPOND&eid=NXBkN2h2bG9xMW5yMHVoNThxbGUzZnVyYWsgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&rst=3&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWM4MTVhNDhjOTE0YmE4MjVlMzg0ODQyN2Q4MTFmZTlkYWZlYjdhNjI&ctz=Europe%2FBerlin&hl=en&es=0" style="color:#20c;white-space:nowrap" itemprop="url">Maybe</a></span></span><span style="margin:0 0.4em;font-weight:normal"> - </span><span itemprop="potentialaction" itemscope itemtype="http://schema.org/RsvpAction"><meta itemprop="attendance" content="http://schema.org/RsvpAttendance/No"/><span itemprop="handler" itemscope itemtype="http://schema.org/HttpActionHandler"><link itemprop="method" href="http://schema.org/HttpRequestMethod/GET"/><a href="https://www.google.com/calendar/event?action=RESPOND&eid=NXBkN2h2bG9xMW5yMHVoNThxbGUzZnVyYWsgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&rst=2&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWM4MTVhNDhjOTE0YmE4MjVlMzg0ODQyN2Q4MTFmZTlkYWZlYjdhNjI&ctz=Europe%2FBerlin&hl=en&es=0" style="color:#20c;white-space:nowrap" itemprop="url">No</a></span></span></strong>    <wbr><a href="https://www.google.com/calendar/event?action=VIEW&eid=NXBkN2h2bG9xMW5yMHVoNThxbGUzZnVyYWsgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWM4MTVhNDhjOTE0YmE4MjVlMzg0ODQyN2Q4MTFmZTlkYWZlYjdhNjI&ctz=Europe%2FBerlin&hl=en&es=0" style="color:#20c;white-space:nowrap" itemprop="url">more options »</a></p></td></tr><tr><td style="background-color:#f6f6f6;color:#888;border-top:1px Solid #ccc;font-family:Arial,Sans-serif;font-size:11px"><p>Invitation from <a href="https://www.google.com/calendar/" target="_blank" style="">Google Calendar</a></p><p>You are receiving this courtesy email at the account club2@mailbroy.informatik.tu-muenchen.de because you are an attendee of this event.</p><p>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.</p><p>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. <a href="https://support.google.com/calendar/answer/37135#forwarding">Learn More</a>.</p></td></tr></table></div></span></span>