Unbounded Model-Checking with Interpolation for Regular Language Constraints. Gange, G., Navas, J. A., Stuckey, P. J., Søndergaard, H., & Schachte, P. In Piterman, N. & Smolka, S., editors, TACAS 2013: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 7795, of Lecture Notes in Computer Science, pages 277–291, 2013. Springer.
doi  abstract   bibtex   
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, \sysrevenant, 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 \textscrevenant 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.
@InProceedings{Gan-Nav-Stu-Son-Sch_TACAS13,
  author    = {Graeme Gange and 
		Jorge A. Navas and 
		Peter J. Stuckey and 
		Harald S{\o}ndergaard and 
		Peter Schachte},
  title     = {Unbounded Model-Checking with Interpolation for Regular
                Language Constraints},
  editor    = {N. Piterman and S. Smolka},
  booktitle = {TACAS 2013: Proceedings of the 19th International
		Conference on Tools and Algorithms for the Construction 
		and Analysis of Systems},
  series    = {Lecture Notes in Computer Science},
  volume    = {7795},
  pages     = {277--291},
  publisher = {Springer},
  year      = {2013},
  doi       = {10.1007/978-3-642-36742-7_20},
  abstract  = {We present a decision procedure for the problem of, 
		given a set of regular expressions $R_1, \ldots, R_n$,
		determining whether $R = R_1 \cap \cdots \cap R_n$ is 
		empty.  Our solver, \sys{revenant}, finitely unrolls 
		automata for $R_1, \ldots, 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 \textsc{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.},
  keywords  = {Static analysis, Formal languages, Model checking, Interpolants, String constraints},
}

Downloads: 0