On the Automatic Verification of Dynamic/Parametrized Systems

Опубликовано 6 сентября 2016, 17:43

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.