[Club2] Invitation: Formal Proof and Analysis of an Incremental Cycle Detecti... @ Wed Jun 5, 2019 14:00 - 15:00 (CEST) (club2 at mailbroy.informatik.tu-muenchen.de)
julianbrunner at gmail.com
julianbrunner at gmail.com
Tue May 28 23:59:03 CEST 2019
You have been invited to the following event.
Title: Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
Speaker: Armaël Guéneau
Abstract
In this talk, I will present the analysis of a state-of-the-art incremental
cycle detection algorithm due to Bender, Fineman, Gilbert, and Tarjan. The
algorithm maintains subtle invariants, and features a highly non trivial
asymptotic, amortized complexity bound. We propose a simple change that
allows the algorithm to be regarded as genuinely online. Then, I will
detail how we exploit Separation Logic with Time Credits to simultaneously
verify the correctness and the worst-case amortized complexity of the
modified algorithm. This will be the occasion of deeper dives explaining
our approach for modular verification of asymptotic complexity using time
credits, in the context of the Coq proof assistant.
This is joint work with Arthur Charguéraud, Jacques-Henri Jourdan and
François Pottier.
When: Wed Jun 5, 2019 14:00 – 15:00 Central European Time - Berlin
Where: MI 02.07.023
Calendar: club2 at mailbroy.informatik.tu-muenchen.de
Who:
* julianbrunner at gmail.com - creator
* puma-alle at lists.tcs.ifi.lmu.de
* club2 at mailbroy.informatik.tu-muenchen.de
* casasa at in.tum.de
* armael.gueneau at inria.fr
Event details:
https://www.google.com/calendar/event?action=VIEW&eid=NXJwYTVwMjhwZzlwZWs2MWh0NGQyMGQ1bWQgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTg1MDNjNjFlZDRkODhiODM5NDFmY2M1M2MwNDA1YmE2M2M2YWFkZWM&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/20190528/4d6c7da1/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2882 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20190528/4d6c7da1/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2942 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20190528/4d6c7da1/attachment.bin>
More information about the Club2
mailing list