Finite automata and their derivatives, as well as various logical theories, are a major enabling concept for automated SW engineering (ASE) methods (and not only them). However, to realize their theoretical potential, algorithms and heuristics that would solve computationally hard problems in practical instances are still needed. A prominent role in many ASE methods, such as SW model checking or symbolic execution, is played by automated solving of formulae in various theories of first-order logic, the so-called SMT solving. Currently existing state-of-the-art SMT solvers, such as CVC5 or Z3, can in many cases quickly decide satisfiability of formulae in many (usually quantifier-free) theories. Reasoning about programs with higher-level data structures, such as strings or dynamic memory, however, requires the use of more complex theories, such as the SMT theory of strings, separation logic, or theories with quantifiers, where current solvers lack in performance. In many of such cases, efficient techniques of dealing with automata would help.
