Mercredi 16 Octobre, 11h en salle Aurigny
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
We study a state-of-the-art incremental cycle detection algorithm due to Bender, Fineman, Gilbert,and Tarjan. We propose a simple change that allows the algorithm to be regarded as genuinelyonline. Then, we exploit Separation Logic with Time Credits to simultaneously verify the correctnessand the worst-case amortized asymptotic complexity of the modified algorithm. Joint work with Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier.
Exposés des semaines suivantes
Jeudi 7 Novembre, 14h en salle Lipari (a confirmer)
On the Monniaux Problem in Abstract Interpretation
The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program P, a safety (e.g., non-reachability) specification φ, and an abstract domain of invariants D, does there exist an inductive invariant in D guaranteeing that program P meets its specification φ. The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers. In this talk, I’ll present a select overview and survey of work on this problem, and discuss some recent results for semilinear invariants for unguarded affine programs.
Jeudi 14 Novembre, 14h en salle Aurigny (a confirmer)
An Implicit Structural Analysis Method for Multi-Mode DAE Systems
The Modelica mathematical modeling language, based on Differential Algebraic Equations (DAE), brings several specific issues that do not exist with modeling languages based on Ordinary Differential Equations. The main problem is the determination of the differentiation index and of the latent equations. Prior to generating simulation code and calling solvers, the compilation of a Modelica model requires a structural analysis step, which reduces the differentiation index to a level acceptable by numerical solvers. The Modelica language allows hybrid models with multiple modes, mode-dependent dynamics and state-dependent mode switching. These Multimode DAE (mDAE) systems are much harder to deal with. The main difficulties are (i) the combinatorial explosion of the number of modes and (ii) the correct handling of mode switchings. In this talk, we focus on the first issue, namely: How can we perform a structural analysis of a mDAE in all possible modes, without enumerating these modes? We present a structural analysis algorithm for mDAE systems, based on an implicit representations of the varying structure of a mDAE. It generalizes J. Pryce's Sigma-method to the multimode case and uses Binary Decision Diagrams (BDD) to represent the mode-dependent structure of a mDAE. The algorithm determines, as a function of the mode, the set a latent equations, the leading variables and the state vector. This is then used to compute a mode-dependent block-triangular decomposition of the system, that can be used to generate simulation code with a mode-dependent scheduling of the blocks of equations.
Lundi 25 Novembre, 14h
Game Theory, Evolution and Networks
In classical game theory, the players are rational agents who aim at maximising their individual gains. Their rational choices lead them to play equilibira (such as the famous Nash equilibrium). We will then turn our attention to evolutionary game theory whose initial goal was to study the evolution of populations in biology. In this evolutionary framework, the players are not supposed to be rational anymore. The agents are now genetically programmed to play in a certain way. The focus is no more on the interactions between two agents, but rather on the evolution of a large population composed of numerous agents of two types. We will see that although classical game theory and evolutionary game theory have fundamental differences, they share common features. We will conclude the talks with recent work where we try to identify a theoretical framework inspired from game theory, in order to apply it to interdomain routing problems. This is a joint work with Gilles Geeraerts, Marion Hallet, Benjamin Monmenge and Bruno Quoitin.
Vos propositions sont les bienvenues !