×

Computing minimal separating DFAs and regular invariants using SAT and SMT solvers. (English) Zbl 1374.68264

Chakraborty, Supratik (ed.) et al., Automated technology for verification and analysis. 10th international symposium, ATVA 2012, Thiruvananthapuram, India, October 3–6, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33385-9/pbk). Lecture Notes in Computer Science 7561, 354-369 (2012).
Summary: 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.
For the entire collection see [Zbl 1251.68006].

MSC:

68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
90C10 Integer programming

Software:

InvGen
PDFBibTeX XMLCite
Full Text: DOI