On the Automatic Verification of Dynamic/Parametrized Systems

  • Ahmed Bouajjani | University Paris Diderot

We give an overview on automatic verification of infinite-state systems in general and in particular of dynamic/parametrized networks of processes. We present (some of) the main existing approaches based on symbolic techniques with automata/logic based formalisms for reasoning about infinite sets of configurations. We show the application of the presented techniques in the verification of various classes of systems/programs (such as concurrent programs with dynamic creation of processes, programs with dynamic heaps, programs with arrays, etc.). The talk refers to recently published work, as well as to on-going work.

Speaker Details

Ahmed Bouajjani is a full Professor in Computer Science at the University Paris Diderot (Paris 7), and he is the head of the Verification group at Liafa (a joint laboratory of CNRS and the University of Paris 7). Previously, he was Associate Professor at the University Joseph Fourier (Grenoble) and a member of the Verimag laboratory. He was researcher on leave at CNRS in 1994-1996. He got his PhD and his “Habilitation” in Computer Science from the University Joseph Fourier (Grenoble). His research interests include: Formal modeling and verification methods, algorithmic verification of infinite-state systems, program verification, automata and logics. (URL: http://www.liafa.jussieu.fr/~abou)

Watch Next