The formal relation between logic and automata has been established by the seminal works of Buechi and Rabin, between automata on (infinite) words and trees and Monadic Second order Logic (SkS). This relation provides elegant automata-theoretic decidability proofs for some of the most general logics known to be decidable.
This line of work builds on the logic-automata connection and reduces program verification problems such as safety, liveness and validity of Hoare triples to reachability and termination problems for various types of automata, such as counter machines, tree automata, etc.
The research problems currently addressed are:
- complexity of the reachability and termination for flat counter machines,
- extended models involving recursion and branching (Horn clauses)
- decision procedures for array logics and verification of programs with arrays
- logics for programs with recursive dynamically allocated data structures (lists, trees, and beyond)
Current projects
People involved
