Verification by automata and acceleration-based approaches
monniaux · 2015
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 (...)