Algorithmic verification of infinite-state 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 well-known 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 low-power 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 "push-button" 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 infinite-state 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 Paris-Saclay 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:
|
|
|
||||||||||||||||