Automata-theoretic methods for infinite-state verification
(summer term 2015)

Lectures

1. Introduction to Tree Automata -- the original slides by Florent Jacquemard are available here, the TATA book is available here.
2. Simulation-based Reduction of Nondeterministic Automata.
3. Antichain-based Inclusion on Nondeterministic Automata.
   • Downward Antichain-based Inclusion on Nondeterministic Tree Automata.
   • The VATA library implementing many of the inclusion checking algorithms combining antichains and simulations (including their semi-symbolic versions).
4. Congruence-based Inclusion on Nondeterministic Word Automata.
   • Checking NFA equivalence with bisimulations up to congruence: web page of Filippo Bonchi and Damien Pous devoted to the result, including a technical report with its detailed description and an applet demonstrating the method. There is also a video about the authors and the method.
   • The VATA library contains an implementation of the approach (so far, for word automata only).
5. Abstract regular (tree) model checking.
   • A very prototypical generic tool for abstract regular tree model checking based on nondeterministic tree automata, implemented using Ocaml/Timbuk, is available here.
   • A prototype tool applying ARTMC based on deterministic tree automata from the MONA library for verification of programs with complex dynamic linked data structures is available here. This tool is based on a decompositon of heap graphs into tree backbones and routing expressions.
6. Forest automata for shape analysis.
   • The above approach is implemented in the Forester tool. The extension with data is currently not available, a support for predicate language abstraction and counterexample validation is under way.
7. Deciding separation logic with inductive list predicates via TA membership.
   • The associated tool called SPEN is available here.
8. Deciding separation logic with inductive list predicates via TA inclusion.
   • The associated tool called SLIDE is available here.
9. Deciding WS1S through nondeterministic automata.
   • The MONA tool for deciding WS1S and WS2S formulae via deterministic semi-symbolic word and tree automata.
   • The dWiNA tool for deciding WS1S using nondeterministic word automata and antichains.