Skip to main content
SpringerLink
Log in

A Local Greibach Normal Form for Hyperedge Replacement Grammars

  • Conference paper
Language and Automata Theory and Applications (LATA 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6638))

Abstract

Heap-based data structures play an important role in modern programming concepts. However standard verification algorithms cannot cope with infinite state spaces as induced by these structures. A common approach to solve this problem is to apply abstraction techniques. Hyperedge replacement grammars provide a promising technique for heap abstraction as their production rules can be used to partially abstract and concretise heap structures. To support the required concretisations, we introduce a normal form for hyperedge replacement grammars as a generalisation of the Greibach Normal Form for string grammars and the adapted construction.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bakewell, A., Plump, D., Runciman, C.: Checking the shape safety of pointer manipulations. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 48–61. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular Tree Model Checking. ENTCS 149, 37–48 (2006)

    MathSciNet  MATH  Google Scholar 

  3. Distefano, D., Katoen, J.P., Rensink, A.: Safety and liveness in concurrent pointer programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 280–312. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Dodds, M.: From Separation Logic to Hyperedge Replacement and Back. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 484–486. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Dumitrescu, S.: Several Aspects of Context Freeness for Hyperedge Replacement Grammars. W. Trans. on Comp. 7, 1594–1604 (2008)

    Google Scholar 

  6. Engelfriet, J.: A Greibach Normal Form for Context-free Graph Grammars. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 138–149. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  7. Habel, A.: Hyperedge Replacement: Grammars and Languages. Springer, New York (1992)

    MATH  Google Scholar 

  8. Heinen, J., Noll, T., Rieger, S.: Juggrnaut: Graph Grammar Abstraction for Unbounded Heap Structures. In: TTSS 2009 (2009) (to be published in ENTCS)

    Google Scholar 

  9. Klempien-Hinrichs, R.: Normal Forms for Context-Free Node-Rewriting Hypergraph Grammars. Math. Structures in Comp. Sci. 12, 135–148 (2002)

    MathSciNet  MATH  Google Scholar 

  10. O’Hearn, P.W., Hongseok, Y., Reynolds, J.C.: Separation and Information Hiding. In: POPL 2004, vol. 39, pp. 268–280 (2004)

    Google Scholar 

  11. Rensink, A.: Canonical Graph Shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 401–415. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Rensink, A.: Summary from the Outside In. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 486–488. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  13. Rensink, A., Distefano, D.: Abstract Graph Transformation. In: SVV 2005, vol. 157, pp. 39–59 (2006)

    Google Scholar 

  14. Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS 2002, pp. 55–74 (2002)

    Google Scholar 

  15. Rieger, S., Noll, T.: Abstracting Complex Data Structures by Hyperedge Replacement. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 69–83. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Rozenberg, G.: Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1. World Scientific Publishing Co., Inc., River Edge (1997)

    Book  MATH  Google Scholar 

  17. Rozenberg, G., Welzl, E.: Boundary NLC Graph Grammars-Basic Definitions, Normal Forms, and Complexity. Inf. Control 69, 136–167 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  18. Sagiv, M., Reps, T., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic. ACM Trans. Program. Lang. Syst. 24, 217–298 (2002)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Modeling and Verification Group, RWTH Aachen University, Germany

    Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen & Thomas Noll

Authors
  1. Christina Jansen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jonathan Heinen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Joost-Pieter Katoen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Thomas Noll
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Research Group on Mathematical Linguistics, Universitat Rovira i Virgili, Avinguda Catalunya, 35, 43002, Tarragona, Spain

    Adrian-Horia Dediu  & Carlos Martín-Vide  & 

  2. Department of Informatics, Kyushu University, 744 Motooka, 819–0395, Fukuoka, Japan

    Shunsuke Inenaga

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jansen, C., Heinen, J., Katoen, JP., Noll, T. (2011). A Local Greibach Normal Form for Hyperedge Replacement Grammars. In: Dediu, AH., Inenaga, S., Martín-Vide, C. (eds) Language and Automata Theory and Applications. LATA 2011. Lecture Notes in Computer Science, vol 6638. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21254-3_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-21254-3_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-21253-6

  • Online ISBN: 978-3-642-21254-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation