TY - GEN

T1 - Unbounded model-checking with interpolation for regular language constraints

AU - Gange, Graeme

AU - Navas, Jorge A.

AU - Stuckey, Peter J.

AU - Søndergaard, Harald

AU - Schachte, Peter

PY - 2013/3/5

Y1 - 2013/3/5

N2 - We present a decision procedure for the problem of, given a set of regular expressions R 1, ..., R n , determining whether R = R 1 ∩ ... ∩ R n is empty. Our solver, revenant, finitely unrolls automata for R 1, ... , 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.

AB - We present a decision procedure for the problem of, given a set of regular expressions R 1, ..., R n , determining whether R = R 1 ∩ ... ∩ R n is empty. Our solver, revenant, finitely unrolls automata for R 1, ... , 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.

UR - http://www.scopus.com/inward/record.url?scp=84874446278&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-36742-7_20

DO - 10.1007/978-3-642-36742-7_20

M3 - Conference Paper

AN - SCOPUS:84874446278

SN - 9783642367410

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 277

EP - 291

BT - Tools and Algorithms for the Construction and Analysis of Systems - 19th Int. Conf., TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.

PB - Springer

T2 - 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013

Y2 - 16 March 2013 through 24 March 2013

ER -