Skip to main content

2021 | OriginalPaper | Buchkapitel

Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars

verfasst von : Ira Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte

Erschienen in: Graph Transformation

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We present a tool that checks for a given context-free graph grammar whether the corresponding graph reduction system in which all rules are applied backward, is confluent—a question that arises when using graph grammars to guide state space abstractions for analyzing heap-manipulating programs; confluence of the graph reduction system then guarantees the abstraction’s uniqueness. If a graph reduction system is not confluent, our tool provides symbolic representations of counterexamples to confluence, i.e., non-joinable critical pairs, for manual inspection. Furthermore, it features a heuristics-based completion procedure that attempts to turn a graph reduction system into a confluent one without invalidating the properties mandated by the abstraction framework. We evaluate our implementation on various graph grammars for verifying data structure traversal algorithms from the literature.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
4
That is, rules 2 and 3 were applied. To improve performance, Attestor generates specialized rules in which two or more external nodes are identical; the number after the dot indicates which case of a rule has been applied.
 
Literatur
8.
Zurück zum Zitat Deckwerth, F.: Static Verification Techniques for Attributed Graph Transformations. Ph.D. thesis, Technische Universität, Darmstadt (2017) Deckwerth, F.: Static Verification Techniques for Attributed Graph Transformations. Ph.D. thesis, Technische Universität, Darmstadt (2017)
9.
Zurück zum Zitat Drewes, F., Kreowski, H.J., Habel, A.: Hyperedge replacement graph grammars. In: Handbook of Graph Grammars and Computing by Graph Transformation, vol. I: Foundations, pp. 95–162. World Scientific (1997) Drewes, F., Kreowski, H.J., Habel, A.: Hyperedge replacement graph grammars. In: Handbook of Graph Grammars and Computing by Graph Transformation, vol. I: Foundations, pp. 95–162. World Scientific (1997)
12.
Zurück zum Zitat Heinen, J., Jansen, C., Katoen, J.P., Noll, T.: Verifying pointer programs using graph grammars. Sci. Comput. Programm. 97(1), 157–162 (2015)CrossRef Heinen, J., Jansen, C., Katoen, J.P., Noll, T.: Verifying pointer programs using graph grammars. Sci. Comput. Programm. 97(1), 157–162 (2015)CrossRef
13.
Zurück zum Zitat Hoffmann, B., Plump, D.: Implementing term rewriting by jungle evaluation. RAIRO Theor. Inform. Appl. 25, 445–472 (1991)MathSciNetCrossRef Hoffmann, B., Plump, D.: Implementing term rewriting by jungle evaluation. RAIRO Theor. Inform. Appl. 25, 445–472 (1991)MathSciNetCrossRef
15.
Zurück zum Zitat Jansen, C.: Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic. Ph.D. thesis, RWTH Aachen University, Germany (2017) Jansen, C.: Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic. Ph.D. thesis, RWTH Aachen University, Germany (2017)
17.
Zurück zum Zitat Knuth, D., Bendix, P.: Simple word problems in universal algebra. Computational Problems in Abstract Algebra, pp. 263–297 (1970) Knuth, D., Bendix, P.: Simple word problems in universal algebra. Computational Problems in Abstract Algebra, pp. 263–297 (1970)
18.
Zurück zum Zitat Lambers, L., Born, K., Kosiol, J., Strüber, D., Taentzer, G.: Granularity of conflicts and dependencies in graph transformation systems: a two-dimensional approach. J. Logic. Algebraic Meth. Program. 103, 105–129 (2019)MathSciNetCrossRef Lambers, L., Born, K., Kosiol, J., Strüber, D., Taentzer, G.: Granularity of conflicts and dependencies in graph transformation systems: a two-dimensional approach. J. Logic. Algebraic Meth. Program. 103, 105–129 (2019)MathSciNetCrossRef
19.
Zurück zum Zitat Lambers, L., Ehrig, H., Orejas, F.: Conflict detection for graph transformation with negative application conditions. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 61–76. Springer, Heidelberg (2006). https://doi.org/10.1007/11841883_6CrossRefMATH Lambers, L., Ehrig, H., Orejas, F.: Conflict detection for graph transformation with negative application conditions. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 61–76. Springer, Heidelberg (2006). https://​doi.​org/​10.​1007/​11841883_​6CrossRefMATH
20.
Zurück zum Zitat Lambers, L., Ehrig, H., Orejas, F.: Efficient conflict detection in graph transformation systems by essential critical pairs. Electron. Notes Theor. Comput. Sci. 211, 17–26 (2008)CrossRef Lambers, L., Ehrig, H., Orejas, F.: Efficient conflict detection in graph transformation systems by essential critical pairs. Electron. Notes Theor. Comput. Sci. 211, 17–26 (2008)CrossRef
21.
Zurück zum Zitat Matheja, C.: Automated reasoning and randomization in separation logic. Ph.D. thesis, RWTH Aachen University, Germany (2020) Matheja, C.: Automated reasoning and randomization in separation logic. Ph.D. thesis, RWTH Aachen University, Germany (2020)
23.
Zurück zum Zitat Plump, D.: Confluence of graph transformation revisited. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 280–308. Springer, Heidelberg (2005). https://doi.org/10.1007/11601548_16CrossRef Plump, D.: Confluence of graph transformation revisited. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 280–308. Springer, Heidelberg (2005). https://​doi.​org/​10.​1007/​11601548_​16CrossRef
24.
Zurück zum Zitat Plump, D.: Checking graph-transformation systems for confluence. ECEASST 26 (2010) Plump, D.: Checking graph-transformation systems for confluence. ECEASST 26 (2010)
Metadaten
Titel
Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars
verfasst von
Ira Fesefeldt
Christoph Matheja
Thomas Noll
Johannes Schulte
Copyright-Jahr
2021
DOI
https://doi.org/10.1007/978-3-030-78946-6_15