Skip to main content
main-content

Tipp

Weitere Kapitel dieses Buchs durch Wischen aufrufen

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

share
TEILEN

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.
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
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)
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

Premium Partner