Computing minimal separating DFAs and regular invariants using SAT and SMT solvers

Abstract

We develop a generic technique to compute minimal separating DFAs (deterministic finite automata) and regular invariants. Our technique works by expressing the desired properties of a solution in terms of logical formulae and using SAT or SMT solvers to find solutions. We apply our technique to three concrete problems: computing minimal separating DFAs (e.g., used in compositional verification), regular model checking, and synthesizing loop invariants of integer programs that are expressible in Presburger arithmetic. © 2012 Springer-Verlag.