(The lecturer of this course will be Prof. Tomáš Vojnar, Brno University of Technology)
The course will present a series of recent results from the area of dealing efficiently with non-deterministic finite word and tree automata together with their selected applications in the areas of infinite-state verification and decision procedures. In particular, methods for reducing the size of non-deterministic word and tree automata based on various advanced notions of simulations will be presented first. Next, methods based on antichains and congruences (both combined with simulations) for checking inclusion without explicitly determinising the involved automata will be presented. Subsequently, the notion of forest automata and its application in the area of shape analysis will be discussed. Finally, several decision procedures based on dealing with non-deterministic automata will be presented: two of them for checking entailment in fragments of separation logic with inductive predicates, and one for deciding WS1S formulae. The discussed methods have been implemented in tools such as VATA, Forester, Spen, Slide, and dWiNA, with which the students are expected to experiment within the course.
Automata-based methods. Abstract regular model checking, forest automata for shape analysis, efficient techniques for dealing with automata, decision procedures for separation logic and WSkS based on nondeterministic automata, our works on symbolic memory graphs.
