Title: Abstract Regular (Tree) Model Checking
By: Tomas Vojnar (Brno University of Technology)
Abstract:
Regular model checking is a generic technique for verification of infinite-state and/or parametrised systems (including software, hardware, or protocols with unbounded recursion, communication buffers, unbounded numbers of processes, unbounded counters, unbounded dynamic linked data structures, etc.). The approach uses finite word automata or finite tree automata to finitely represent potentially infinite sets of reachable configurations of the systems being verified. The problems addressed by regular model checking are typically undecidable. In order to facilitate termination in as many cases as possible, some kind of acceleration is needed in the incremental computation of the set of reachable configurations in regular model checking. In this lecture, we in particular describe how various incrementally refinable abstractions on finite (word and tree) automata can be used for this purpose. Moreover, the use of abstraction does not only increase chances of the technique to terminate, but it also significantly reduces the problem of an explosion in the number of states of the automata that are generated by regular model checking. We illustrate possible applications of abstract regular model checking on examples from parameterized verification (e.g., verification of various kinds of mutual exclusion protocols), shape analysis (verification of programs with lists, trees, and even more complex data structures), as well as hardware verification (verification of pipelined microprocessors).
Short bio:
Tomas Vojnar received his PhD at the Brno University of Technology (BUT) in 2001. From 2001 to 2003, he worked as a postdoc researcher at LIAFA, Université Paris Diderot. Since 2003, he works at the Faculty of Information Technology of BUT. He defended his habilitation thesis in 2007 and became a full professor in 2012. His research focuses mainly on automated analysis and verification, especially over infinite-state and concurrent systems. In the former area, his work has included formal verification of parameterized systems, abstract regular model checking, shape analysis of programs with pointers and dynamic linked data structures, as well as verification of hardware designs. He has also worked on efficient ways of dealing with various kinds of non-deterministic automata and logics, with applications in the above mentioned verification approaches. As for concurrent programs, he has mainly worked in the area of their noise-based testing and dynamic analysis, self-healing, and applications of search techniques in noise-based testing. He has (co-)authored over 100 scientific publications as well as multiple software tool prototypes (e.g., Forester, Predator, SearchBestie, AnaConDA, Spen, Slide, or dWiNA). These works won multiple best paper awards, such as the EATCS Best Theory Paper Award of ETAPS'10, the best tool paper of RV'12, as well as multiple medals in the international software verification competition SV-COMP'12-15, including a Goedel medal at the FLoC Olympic Games 2014.