Unbounded model-checking with interpolation for regular language constraints.(English)Zbl 1381.68162

Piterman, Nir (ed.) et al., Tools and algorithms for the construction and analysis of systems. 19th international conference, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-36741-0/pbk). Lecture Notes in Computer Science 7795, 277-291 (2013).
Summary: We present a decision procedure for the problem of, given a set of regular expressions $$R _{1}, \dots ,R _{n }$$, determining whether $$R = R _{1} \cap \dots \cap R _{n }$$ is empty. Our solver, revenant, finitely unrolls automata for $$R _{1}, \dots ,R _{n }$$, encoding each as a set of propositional constraints. If a SAT solver determines satisfiability then $$R$$ is non-empty. Otherwise our solver uses unbounded model checking techniques to extract an interpolant from the bounded proof. This interpolant serves as an overapproximation of $$R$$. If the solver reaches a fixed-point with the constraints remaining unsatisfiable, it has proven $$R$$ to be empty. Otherwise, it increases the unrolling depth and repeats. We compare revenant with other state-of-the-art string solvers. Evaluation suggests that it behaves better for constraints that express the intersection of sets of regular languages, a case of interest in the context of verification.
For the entire collection see [Zbl 1268.68030].

MSC:

 68Q60 Specification and verification (program logics, model checking, etc.) 68Q45 Formal languages and automata 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

HAMPI; FOCI; MAGIC
Full Text: