×

zbMATH — the first resource for mathematics

Interactive and automated proofs for graph transformations. (English) Zbl 1398.68286
Summary: This article explores methods to provide computer support for reasoning about graph transformations. We first define a general framework for representing graphs, graph morphisms and single graph rewriting steps. This setup allows for interactively reasoning about graph transformations. In order to achieve a higher degree of automation, we identify fragments of the graph description language in which we can reduce reasoning about global graph properties to reasoning about local properties, involving only a bounded number of nodes, which can be decided by Boolean satisfiability solving or even by deterministic computation of low complexity.

MSC:
68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Arendt, T.; Biermann, E.; Jurack, S.; Krause, C.; Taentzer, G., (2010)
[2] Asztalos, M.; Lengyel, L.; Levendovszky, T., (2010)
[3] Balbiani, P.; Echahed, R.; Herzig, A.; Ehrig, H.; Rensink, A.; Rozenberg, G.; Schürr, A., Graph Transformations, A dynamic logic for termgraph rewriting, 59-74, (2010), Springer: Springer, Berlin/Heidelberg
[4] Baldan, P.; Corradini, A.; Esparza, J.; Heindel, T.; König, B.; Kozioura, V., (2005)
[5] Baldan, P.; Corradini, A.; König, B., A framework for the verification of infinite-state graph transformation systems, Information and Computation, 206, 869-907, (2008) · Zbl 1153.68034
[6] Ballarin, C.; Berardi, S.; Coppo, M.; Damiani, F., Types for Proofs and Programs, Locales and locale expressions in Isabelle/Isar, 34-50, (2004), Springer: Springer, Berlin/Heidelberg
[7] Berdine, J.; Calcagno, C.; O’Hearn, P.; Lodaya, K.; Mahajan, M., FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, A decidable fragment of separation logic, 110-117, (2004), Springer: Springer, Berlin/Heidelberg
[8] Courcelle, B.; Irène, Durand A.; Rhodes, C., (2010)
[9] Courcelle, B.; Engelfriet, J., Graph Structure and Monadic Second-Order Logic, A Language Theoretic Approach, (2011), Cambridge University Press
[10] Da, Costa, S. A.; Ribeiro, L., Formal verification of graph grammars using mathematical induction, Electronic Notes in Theoretical Computer Science, 240, 43-60, (2009) · Zbl 1347.68243
[11] Da, Costa, S.; Ribeiro, L., Verification of graph grammars using a logical approach, Science of Computer Programming, 77, 480-504, (2012) · Zbl 1243.68211
[12] De, Bruijn, N. G., Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, Indagationes Mathematicae, 34, 381-392, (1972) · Zbl 0253.68007
[13] Ehrig, H.; Heckel, R.; Korff, M.; Löwe, M.; Ribeiro, L.; Wagner, A.; Corradini, A.; Rozenberg, G., Handbook of Graph Grammars, Algebraic approaches to graph transformation - Part II: Single pushout approach and comparison with double pushout approach, 247-312, (1997), World Scientific
[14] Ghamarian, A.; De, Mol, M.; Rensink, A.; Zambon, E.; Zimakova, M., Modelling and analysis using GROOVE, International Journal on Software Tools for Technology Transfer, 14, 15-40, (2012)
[15] Habel, A.; Pennemann, K.-H., Correctness of high-level transformation systems relative to nested conditions, Mathematical Structures in Computer Science, 19, 245-296, (2009) · Zbl 1168.68022
[16] Habel, A.; Pennemann, K.-H.; Rensink, A.; Corradini, A.; Ehrig, H.; Montanari, U.; Ribeiro, L.; Rozenberg, G., Graph Transformations (ICGT), Natal, Brazil, Weakest preconditions for high-level programs, 445-560, (2006), Springer Verlag: Springer Verlag, Berlin · Zbl 1156.68347
[17] Hosoya, H., XML Processing - The Tree-Automata Approach, (2011), Cambridge University Press · Zbl 1235.68004
[18] Immerman, N.; Rabinovich, A.; Reps, T.; Sagiv, M.; Yorsh, G.; Marcinkowski, J.; Tarlecki, A., Computer Science Logic, The boundary between decidability and undecidability for transitive-closure logics, 160-174, (2004), Springer: Springer, Berlin/Heidelberg · Zbl 1095.03008
[19] Mcpeak, S.; Necula, G.; Etessami, K.; Rajamani, S., Computer Aided Verification, Data structure specifications via local equality axioms, 476-490, (2005), Springer: Springer, Berlin/Heidelberg · Zbl 1081.68584
[20] Møller, A.; Schwartzbach, M. I., 221-231, (2001)
[21] Naraschewski, W.; Wenzel, M.; Grundy, J.; Newey, M., Theorem Proving in Higher Order Logics, Object-oriented verification based on record subtyping in higher-order logic, 349-366, (1998), Springer: Springer, Berlin/Heidelberg · Zbl 0927.03026
[22] Nipkow, T.; Paulson, L.; Wenzel, M., Isabelle/HOL. A Proof Assistant for Higher-Order Logic, (2002), Springer: Springer, Berlin/Heidelberg · Zbl 0994.68131
[23] Orejas, F.; Ehrig, H.; Prange, U., Reasoning with graph constraints, Formal Aspects of Computing, 22, 385-422, (2010) · Zbl 1209.68381
[24] Pennemann, K.-H., (2008)
[25] Pennemann, K.-H.; H., Ehrig; Heckel, R.; Rozenberg, G.; Taentzer, G., Graph Transformations, Resolution-like theorem proving for high-level conditions, 289-304, (2008), Springer: Springer, Berlin/Heidelberg
[26] Poskitt, C. M.; Plump, D., Hoare-style verification of graph programs, Fundamenta Informaticae, 118, 2012-175, (2012) · Zbl 1284.68333
[27] Rensink, A., The joys of graph transformation, Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica, 9, (2005)
[28] Reynolds, J. C., (2002)
[29] Ribeiro, L.; Dotti, F. L.; Da, Costa, S. A.; Dillenburg, F. C., (2010)
[30] Strecker, M.; Mackie, I.; Plump, D., International Workshop on Computing with Terms and Graphs (TERMGRAPH), Modeling and verifying graph transformations in proof assistants, 135-148, (2008), Elsevier Science
[31] Strecker, M.; Varró, D.; Varró, D.; Schürr, A., Pre-Proceedings conf. AGTIVE, Locality in reasoning about graph transformations, (2011), Budapest
[32] Tarski, A., On the calculus of relations, The Journal of Symbolic Logic, 6, 73-89, (1941) · JFM 67.0973.02
[33] Tran, H. N.; Percebois, C., (2012)
[34] Varró, D.; Balogh, A., The model transformation language of the VIATRA2 framework, Science of Computer Programming, 68, 214-234, (2007) · Zbl 1131.68040
[35] Varró, D., Automated formal verification of visual modeling languages by model checking, Journal of Software and Systems Modeling, 3, 85-113, (2004)
[36] Yorsh, G.; Rabinovich, A. M.; Sagiv, M.; Meyer, A.; Bouajjani, A., A logic of reachable patterns in linked data-structures, Journal of Logic and Algebraic Programming, 73, 111-142, (2007) · Zbl 1121.03040
[37] Zambon, E.; Rensink, A., (2011)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.