Automata in Decision Procedures and Formal Verification

In this thesis, we propose a fast reduction of the satisfiability of formulae in the straight-line and acyclic fragments to the emptiness problem of alternating finite-state automata (AFA), which is polynomial in most cases. This reduction, in combination with advanced model checking algorithms such as IC3, provides the first practical algorithm for solving string constraints involving concatenation, finite-state transducers and regular constraints. Furthermore, we introduce a new fragment of string constraints called chain-free and its relaxation called weakly chaninng, along with decision procedures for these fragments. It is important to mention that these new fragments generalize both the straight-line fragment and the acyclic form. Additionally, we presented a method for checking the satisfiability of string constraints, in particular with string-to-number conversion, using parametric flat automata (PFA). This procedure is complemented by an algorithm for converting string constraints to linear formulas in polynomial time with a search space bounded by PFA. In conclusion, we propose and integrate an improved Parikh abstraction into the string solver sloth for solving length constraints.

String solving, Alternating finite automata, Decision procedure, IC3, Satisfiability modulo theories, Program verification, String constraints, Automata, Parikh image.