nach oben

Tipp

Weitere Kapitel dieses Buchs durch Wischen aufrufen

Erschienen in:

Kapitel lesen Erstes Kapitel lesen

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

Einloggen

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel On the Complexity of Simulating Probabilistic Timed Graph Transformation Systems

Nächstes Kapitel GrapePress - A Computational Notebook for Graph Transformations

https://github.com/moves-rwth/attestor.

https://www.user.tu-berlin.de/o.runge/agg/.

https://github.com/moves-rwth/attestor-confluence.

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.

Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: advanced concepts and tools for in-place EMF model transformations. In: Petriu, D.C., Rouquette, N., Haugen, Ø. (eds.) MODELS 2010. LNCS, vol. 6394, pp. 121–135. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16145-2_9 CrossRef

Arndt, H., Jansen, C., Katoen, J.-P., Matheja, C., Noll, T.: Let this graph be your witness!. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 3–11. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_1 CrossRef

Arndt, H., Jansen, C., Matheja, C., Noll, T.: Graph-based shape analysis beyond context-freeness. In: Johnsen, E.B., Schaefer, I. (eds.) SEFM 2018. LNCS, vol. 10886, pp. 271–286. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92970-5_17 CrossRef

Azzi, G.G., Bezerra, J.S., Ribeiro, L., Costa, A., Rodrigues, L.M., Machado, R.: The verigraph system for graph transformation. In: Heckel, R., Taentzer, G. (eds.) Graph Transformation, Specifications, and Nets. LNCS, vol. 10800, pp. 160–178. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75396-6_9 CrossRefMATH

Born, K., Arendt, T., Heß, F., Taentzer, G.: Analyzing conflicts and dependencies of rule-based transformations in Henshin. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 165–168. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46675-9_11 CrossRef

Campbell, G., Plump, D.: Confluence up to garbage. In: Gadducci, F., Kehrer, T. (eds.) ICGT 2020. LNCS, vol. 12150, pp. 20–37. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51372-6_2 CrossRef

Costa, A., et al.: Verigraph: a system for specification and analysis of graph grammars. In: Ribeiro, L., Lecomte, T. (eds.) SBMF 2016. LNCS, vol. 10090, pp. 78–94. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49815-7_5 CrossRef

Deckwerth, F.: Static Verification Techniques for Attributed Graph Transformations. Ph.D. thesis, Technische Universität, Darmstadt (2017)

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)

10.

Fesefeldt, I.: moves-rwth/attestor-confluence. https://github.com/moves-rwth/attestor-confluence/blob/master/readme/HEURISTICS.md

11.

Heckel, R., Küster, J.M., Taentzer, G.: Confluence of typed attributed graph transformation systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 161–176. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45832-8_14 CrossRefMATH

12.

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.

Hoffmann, B., Plump, D.: Implementing term rewriting by jungle evaluation. RAIRO Theor. Inform. Appl. 25, 445–472 (1991) MathSciNetCrossRef

14.

Hristakiev, I., Plump, D.: Checking graph programs for confluence. In: Seidl, M., Zschaler, S. (eds.) STAF 2017. LNCS, vol. 10748, pp. 92–108. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-74730-9_8 CrossRef

15.

Jansen, C.: Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic. Ph.D. thesis, RWTH Aachen University, Germany (2017)

16.

Jansen, C., Heinen, J., Katoen, J.-P., Noll, T.: A local greibach normal form for hyperedge replacement grammars. In: Dediu, A.-H., Inenaga, S., Martín-Vide, C. (eds.) LATA 2011. LNCS, vol. 6638, pp. 323–335. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21254-3_25 CrossRef

17.

Knuth, D., Bendix, P.: Simple word problems in universal algebra. Computational Problems in Abstract Algebra, pp. 263–297 (1970)

18.

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.

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_6 CrossRefMATH

20.

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.

Matheja, C.: Automated reasoning and randomization in separation logic. Ph.D. thesis, RWTH Aachen University, Germany (2020)

22.

Matheja, C., Jansen, C., Noll, T.: Tree-like grammars and separation logic. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 90–108. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26529-2_6 CrossRefMATH

23.

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_16 CrossRef

24.

Plump, D.: Checking graph-transformation systems for confluence. ECEASST 26 (2010)

25.

Runge, O., Ermel, C., Taentzer, G.: AGG 2.0 – new features for specifying and analyzing algebraic graph transformations. In: Schürr, A., Varró, D., Varró, G. (eds.) AGTIVE 2011. LNCS, vol. 7233, pp. 81–88. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34176-2_8 CrossRef

26.

Schulte, J.: Automated Detection and Completion of Confluence for Graph Grammars. Master thesis, RWTH Aachen University, Germany (2019). http://www-i2.informatik.rwth-aachen.de/pub/index.php?type=download&pub_id=1765

27.

Taentzer, G.: AGG: a graph transformation environment for modeling and validation of software. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 446–453. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-25959-6_35 CrossRef

Titel: Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars
verfasst von: Ira Fesefeldt
Christoph Matheja
Thomas Noll
Johannes Schulte
Verlag: Springer International Publishing
Buch: Graph Transformation
Print ISBN: 978-3-030-78945-9

Electronic ISBN: 978-3-030-78946-6

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-78946-6_15

Springer Professional

Tipp

Weitere Kapitel dieses Buchs durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"