@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},
}

{"_id":"HvkxFWy7gJGjYS3ho","bibbaseid":"gange-navas-stuckey-sndergaard-schachte-unboundedmodelcheckingwithinterpolationforregularlanguageconstraints-2013","author_short":["Gange, G.","Navas, J. A.","Stuckey, P. J.","Søndergaard, H.","Schachte, P."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Graeme"],"propositions":[],"lastnames":["Gange"],"suffixes":[]},{"firstnames":["Jorge","A."],"propositions":[],"lastnames":["Navas"],"suffixes":[]},{"firstnames":["Peter","J."],"propositions":[],"lastnames":["Stuckey"],"suffixes":[]},{"firstnames":["Harald"],"propositions":[],"lastnames":["Søndergaard"],"suffixes":[]},{"firstnames":["Peter"],"propositions":[],"lastnames":["Schachte"],"suffixes":[]}],"title":"Unbounded Model-Checking with Interpolation for Regular Language Constraints","editor":[{"firstnames":["N."],"propositions":[],"lastnames":["Piterman"],"suffixes":[]},{"firstnames":["S."],"propositions":[],"lastnames":["Smolka"],"suffixes":[]}],"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, …, 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.","keywords":"Static analysis, Formal languages, Model checking, Interpolants, String constraints","bibtex":"@InProceedings{Gan-Nav-Stu-Son-Sch_TACAS13,\n author = {Graeme Gange and \n\t\tJorge A. Navas and \n\t\tPeter J. Stuckey and \n\t\tHarald S{\\o}ndergaard and \n\t\tPeter Schachte},\n title = {Unbounded Model-Checking with Interpolation for Regular\n Language Constraints},\n editor = {N. Piterman and S. Smolka},\n booktitle = {TACAS 2013: Proceedings of the 19th International\n\t\tConference on Tools and Algorithms for the Construction \n\t\tand Analysis of Systems},\n series = {Lecture Notes in Computer Science},\n volume = {7795},\n pages = {277--291},\n publisher = {Springer},\n year = {2013},\n doi = {10.1007/978-3-642-36742-7_20},\n abstract = {We present a decision procedure for the problem of, \n\t\tgiven a set of regular expressions $R_1, \\ldots, R_n$,\n\t\tdetermining whether $R = R_1 \\cap \\cdots \\cap R_n$ is \n\t\tempty. Our solver, \\sys{revenant}, finitely unrolls \n\t\tautomata for $R_1, \\ldots, R_n$, encoding each as a \n\t\tset of propositional constraints. If a SAT solver \n\t\tdetermines satisfiability then $R$ is non-empty. Otherwise\n\t\tour solver uses unbounded model checking techniques \n\t\tto extract an interpolant from the bounded proof. \n\t\tThis interpolant serves as an overapproximation of $R$. \n\t\tIf the solver reaches a fixed-point with the constraints\n\t\tremaining unsatisfiable, it has proven $R$ to be empty.\n\t\tOtherwise, it increases the unrolling depth and repeats.\n\t\tWe compare \\textsc{revenant} with other state-of-the-art \n\t\tstring solvers. Evaluation suggests that it behaves\n\t\tbetter for constraints that express the intersection of\n\t\tsets of regular languages, a case of interest in the \n\t\tcontext of verification.},\n keywords = {Static analysis, Formal languages, Model checking, Interpolants, String constraints},\n}\n\n","author_short":["Gange, G.","Navas, J. A.","Stuckey, P. J.","Søndergaard, H.","Schachte, P."],"editor_short":["Piterman, N.","Smolka, S."],"key":"Gan-Nav-Stu-Son-Sch_TACAS13","id":"Gan-Nav-Stu-Son-Sch_TACAS13","bibbaseid":"gange-navas-stuckey-sndergaard-schachte-unboundedmodelcheckingwithinterpolationforregularlanguageconstraints-2013","role":"author","urls":{},"keyword":["Static analysis","Formal languages","Model checking","Interpolants","String constraints"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/zarajoy/testbibtex/refs/heads/main/test.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","wpkuJrZJJtqra3FbL","BNGFBQQncqevukxoe"],"keywords":["static analysis","formal languages","model checking","interpolants","string constraints"],"search_terms":["unbounded","model","checking","interpolation","regular","language","constraints","gange","navas","stuckey","søndergaard","schachte"],"title":"Unbounded Model-Checking with Interpolation for Regular Language Constraints","year":2013}