Agenda
June
-
10:0011:00EnglishLaBRI
-
14:0016:30EnglishLaBRI
-
11:0012:00
Colette Johnen (LaBRI)
Title: From Static Stabilization to Dynamic Stabilization in case of bounded recurrent edges
Abstract:
We consider the problem of the Dynamic Simulation, which consists in the design of a transformer that simulates distributed algorithms in a dynamic environment modeled by a dynamic graph. We consider dynamic graphs with a fixed topology, meaning that each existing edge appears infinitely often.
We introduce a self-stabilizing transformer adapted to graphs where every edge appears at least once during τ consecutive synchronous rounds.
Our transformer is minimal in terms of hypotheses in the following sense: solving the Dynamic Simulation Problem in graphs with recurring edges either requires the knowledge of either a bound on the edge recurrency (i.e. τ
), or the knowledge on number of edges.Finally, we introduce the notion of time-bounded stabilization corresponding to pseudo-stabilizing algorithms for which an upper bound on the convergence time depending only of the network's topology.
joint work with Gabriel Le Bouder
EnglishLaBRI 178 -
14:0015:00
Software development is an inherently incremental process. To this end, most programming languages provide basic mechanisms for programmers to indicate that a given functionality is not yet implemented, for instance through dedicated exceptions. Unfortunately, apart from incremental typecheckers, most of the tools used to reason about program correctness—like testing, analysis, and verification frameworks—fail to account for these incompleteness idioms. As a result, programmers are faced with either spurious failure reports or the burden of altering their specifications, which sacrifices the direct causal connection between the code and the reasoning tools. In this talk, I will illustrate this issue in the context of testing, considering both unit testing and property-based testing, as well as certified programming in proof assistants. Examining the problem in such disparate settings allows us to isolate the core concepts required to build truly incremental reasoning tools.
Bio:
Éric Tanter is a Full Professor in the Computer Science Department of the University of Chile. He received his PhD from both the University of Nantes and the University of Chile in 2004. His research interests cover programming languages and software engineering, ranging from the theoretical underpinnings of programming languages to the empirical study of the practice of programming. Recently, he has been deeply involved in the foundations and practice of gradual typing and verification. He holds an Inria International Chair for the period 2025-2029.Salle 178 (LaBRI) -
14:0015:00EnglishLaBRI
-
16:0018:00
The jury consists of the following members:
Tamara Munzner
Raimund Dachselt
Niklas Elmqvist
Caroline Appert
David Auber
Amphi LaBRI