Name
Abstract | ||
|---|---|---|
We present a decision procedure for the problem of, given a set of regular expressions R1, …, Rn, determining whether R=R1∩⋯∩Rn is empty. Our solver, revenant, finitely unrolls automata for R1, …, Rn, 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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-36742-7_20 | TACAS |
Keywords | Field | DocType |
unrolling depth,proven r,decision procedure,bounded proof,propositional constraint,unbounded model-checking,sat solver,unbounded model checking technique,state-of-the-art string solvers,regular expression,regular language constraint,regular language | Intersection (set theory),Discrete mathematics,Regular expression,Model checking,Computer science,Satisfiability,Boolean satisfiability problem,Regular language,Solver,Bounded function | Conference |
Volume | ISSN | Citations |
7795 | 0302-9743 | 6 |
PageRank | References | Authors |
0.47 | 21 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Graeme Gange | 1 | 137 | 24.27 |
| Jorge A. Navas | 2 | 157 | 9.88 |
| Peter J. Stuckey | 3 | 4368 | 457.58 |
| Harald Søndergaard | 4 | 858 | 79.52 |
| Peter Schachte | 5 | 256 | 22.76 |