Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                             Lundi 17 juin, 10h30

                                --------------
                                Armaël Guéneau
                                --------------

                                 Inria Paris

    =====================================================================
    Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
    =====================================================================

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.