A Tool for Intersecting Context-Free Grammars and Its Applications

  • Graeme Gange
  • Jorge A. NavasEmail author
  • Peter Schachte
  • Harald Søndergaard
  • Peter J. Stuckey
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)


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.


Regular Language Bound Model Check Initial Abstraction Multithread Program Regular Approximation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL, pp. 62–73 (2003)Google Scholar
  2. 2.
    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) CrossRefGoogle Scholar
  3. 3.
    Esparza, J., Rossmanith, P., Schwoon, S.: A uniform framework for problems on context-free grammars. Bulletin of the EATCS 72, 169–177 (2000)zbMATHMathSciNetGoogle Scholar
  4. 4.
    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) CrossRefGoogle Scholar
  5. 5.
    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).
  6. 6.
    Hooimeijer, P., Weimer, W.: StrSolve: Solving string constraints lazily. ASE 19(4), 531–559 (2012)Google Scholar
  7. 7.
    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) CrossRefGoogle Scholar
  8. 8.
    Nederhof, M.-J.: Regular approximation of CFLs: a grammatical view. In: Advances in Probabilistic and Other Parsing Technologies, vol. 16, pp. 221–241 (2000)Google Scholar
  9. 9.
    Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: PLDI, pp. 14–24 (2004)Google Scholar
  10. 10.
    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) CrossRefGoogle Scholar
  11. 11.
    Veanes, M., de Halleux, P., Tillmann, N.: Rex: symbolic regular expression explorer. In: ICSTVV, pp. 498–507 (2010)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Graeme Gange
    • 1
  • Jorge A. Navas
    • 2
    Email author
  • Peter Schachte
    • 1
  • Harald Søndergaard
    • 1
  • Peter J. Stuckey
    • 1
  1. 1.The University of MelbourneMelbourneAustralia
  2. 2.NASA Ames Research CenterMoffett FieldUSA

Personalised recommendations