Abstract
This paper describes a tool for intersecting context-free grammars. Since this problem is undecidable the tool follows a refinement-based approach and implements a novel refinement which is complete for regularly separable grammars. We show its effectiveness for safety verification of recursive multi-threaded programs.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL, pp. 62–73 (2003)
Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing c programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 334–349. Springer, Heidelberg (2006)
Esparza, J., Rossmanith, P., Schwoon, S.: A uniform framework for problems on context-free grammars. Bulletin of the EATCS 72, 169–177 (2000)
Gange, G., Navas, J.A., Stuckey, P.J., Søndergaard, H., Schachte, P.: Unbounded model-checking with interpolation for regular language constraints. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 277–291. Springer, Heidelberg (2013)
Gange, G., Navas, J.A., Stuckey, P.J., Søndergaard, H., Schachte, P.: A complete refinement procedure for regular separability of context-free languages (2014). http://people.eng.unimelb.edu.au/gkgange/pubs/cfg_preprint.pdf
Hooimeijer, P., Weimer, W.: StrSolve: Solving string constraints lazily. ASE 19(4), 531–559 (2012)
Long, Z., Calin, G., Majumdar, R., Meyer, R.: Language-theoretic abstraction refinement. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 362–376. Springer, Heidelberg (2012)
Nederhof, M.-J.: Regular approximation of CFLs: a grammatical view. In: Advances in Probabilistic and Other Parsing Technologies, vol. 16, pp. 221–241 (2000)
Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: PLDI, pp. 14–24 (2004)
Suwimonteerabuth, D., Schwoon, S., Esparza, J.: jMoped: a java bytecode checker based on moped. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 541–545. Springer, Heidelberg (2005)
Veanes, M., de Halleux, P., Tillmann, N.: Rex: symbolic regular expression explorer. In: ICSTVV, pp. 498–507 (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J. (2015). A Tool for Intersecting Context-Free Grammars and Its Applications. In: Havelund, K., Holzmann, G., Joshi, R. (eds) NASA Formal Methods. NFM 2015. Lecture Notes in Computer Science(), vol 9058. Springer, Cham. https://doi.org/10.1007/978-3-319-17524-9_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-17524-9_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-17523-2
Online ISBN: 978-3-319-17524-9
eBook Packages: Computer ScienceComputer Science (R0)