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
{"_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":"people.eng.unimelb.edu.au/harald/bibbase.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","wpkuJrZJJtqra3FbL","XqcrNTrCCBr9mSd37"],"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}