Algorithmic verification of infinitestate systems via relaxations
Michael Blondin (UniversitÃ© de Sherbrooke).
Course Summaryy 
About the lecturer 
Location and schedule 
Course materials
Preventing bugs from computer systems is an everlasting quest. Classical software engineering approaches, such as testing, are wellknown to developers and well suited for preventing flaws in sequential systems. Yet, many systems involve interdependent components carrying computations concurrently, e.g. in parallel or in an interleaved fashion. Such concurrent systems are becoming ubiquitous as advances are made, e.g., on multiprocessor architectures, cheap lowpower devices and natural computing. Developing reliable concurrent systems is thus paramount.
Algorithmic verification, also known as model checking, is a powerful method that automatically analyzes a mathematical model abstracting a concrete system. While it offers a "pushbutton" technology, it typically suffers from prohibitive computational complexity, especially for systems with infinite underlying graphs.
In this lecture series, we will learn about challenges in the algorithmic verification of infinitestate systems. More precisely, we will get familiar with Petri nets (also known as vector addition systems): a formalism that allows to reason mathematically about resources evolving concurrently. We will see that while they are difficult to analyze in theory, they admit an elegant theory of relaxations that can be used in a practical algorithmic framework. In particular, we will show that the reachability problem for continuous Petri nets is tractable.
About the lecturer:Michael Blondin is an assistant professor at the UniversitÃ© de Sherbrooke (Canada). Before joining Sherbrooke, he obtained a joint Ph.D. from the ENS ParisSaclay and the UniversitÃ© de MontrÃ©al, and worked as a postdoctoral fellow at the Technical University of Munich. His research interests include automata theory, model checking of concurrent and distributed systems, complexity theory, logic and verification tools. His recent work, which has been published at flagship venues such as LICS and CAV, focuses on the efficient verification of counter systems.
Location and schedule:


