Development of Correct Graph Transformation Systems

 

1 Development of Correct Graph Transformation Systems

Project duration : 2 years

Funded by: German Research Foundation (DFG)

Summary of the research proposal:

For the development of correct graph transformation systems and graph programs, theoretical foundations and resultant concepts are to be developed. As language for the specification of program properties, (instead of formulas of predicate logic) graphical constraints are to be investigated and used as they seem suitable for describing system requirements as well as for inferring conclusions about the behavior of a system. Furthermore, constraint transformation on rules, sets of rules, sequential composition of rules, iterated graph programs are to be investigated and algorithms are to be developed to decide resp. semi-decide the implication problem of graphical constraints. The feasibility and applicability of the above concepts are to be demonstrated by suitable case studies. Accompanying implementations shall take place with the intent to automatize significant steps and, finally, for obtaining a tool for supporting the synthesis of correct graph transformation systems and the verification of graph programs.

 

2 References

2.1 Journal publications

[HP08]

Annegret Habel and Karl-Heinz Pennemann. Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science, 2008. To appear.
[ .pdf ]

2.2 Inproceedings & Incollections

[Aza08]

Karl Azab. Editing nested constraints and application conditions. In A. Habel and M. Mosbah, editors, Proc. Int. Workshop on Graph Computation Models (GCM'08), pages 35-42, 2008. Download Long version.
[ .pdf ]

[Pen08b]

Karl-Heinz Pennemann. Development of correct graph transformation systems - Preliminary abstract. In Graph Transformations (ICGT'08 Doctoral Symposium), volume 5214 of Lecture Notes in Computer Science, pages 508-510. Springer-Verlag, 2008.
[ .pdf ]

[Pen08c]

Karl-Heinz Pennemann. Resolution-like theorem proving for high-level conditions. In Graph Transformations (ICGT'08), volume 5214 of Lecture Notes in Computer Science, pages 289-304. Springer-Verlag, 2008.
[ .pdf ]

[AH08]

Karl Azab and Annegret Habel. High-level programs and program conditions. In Graph Transformations (ICGT'08), volume 5214 of Lecture Notes in Computer Science, pages 211-225. Springer-Verlag, 2008.
[ .pdf ]

[MH08]

Mohamed Mosbah and Annegret Habel. Workshop on graph computation models. In Graph Transformations (ICGT 2008), volume 5214 of Lecture Notes in Computer Science, pages 460-462. Springer, 2008.
[ .pdf ]

[AP08]

Karl Azab and Karl-Heinz Pennemann. Type checking C++ template instantiation by graph programs. In Proc. Int. Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT'08), pages 249-262. Electronic Communications of EASST, 2008.
[ .pdf ]

[Pen08a]

Karl-Heinz Pennemann. An algorithm for approximating the satisfiability problem of high-level conditions. In Proc. Graph Transformation for Verification and Concurrency (GT-VC'07), volume 213 of Electronic Notes in Theoretical Computer Science, pages 75-94. Elsevier, 2008.
[ .pdf ]

[AHPZ07]

Karl Azab, Annegret Habel, Karl-Heinz Pennemann, and Christian Zuckschwerdt. ENFORCe: A system for ensuring formal correctness of high-level programs. In Proc. 3rd International Workshop on Graph Based Tools (GraBaTs'06), volume 1, pages 82-93. Electronic Communications of EASST, 2007.
[ .pdf ]

[HPR06]

Annegret Habel, Karl-Heinz Pennemann, and Arend Rensink. Weakest preconditions for high-level programs. In Graph Transformations (ICGT'06), volume 4178 of Lecture Notes in Computer Science, pages 445-460. Springer-Verlag, 2006.
[ .pdf ]

[HP06]

Annegret Habel and Karl-Heinz Pennemann. Satisfiability of high-level conditions. In Graph Transformations (ICGT'06), volume 4178 of Lecture Notes in Computer Science, pages 430-444. Springer-Verlag, 2006.
[ .pdf ]

[HP05]

Annegret Habel and Karl-Heinz Pennemann. Nested constraints and application conditions for high-level structures. In Hans-Jörg Kreowski, Ugo Montanari, Fernando Orejas, Grzegorz Rozenberg, and Gabriele Taentzer, editors, Formal Methods in Software and System Modeling, volume 3393 of Lecture Notes in Computer Science, pages 294-308. Springer-Verlag, 2005.
[ .ps.gz ]

2.3 Further publications

[AP07]

Karl Azab and Karl-Heinz Pennemann. Type checking C++ template instantiation by graph programs. Berichte aus dem Department für Informatik 04/07, 24 pages, Universität Oldenburg, 2007.
[ .pdf ]

[Zuc06]

Christian Zuckschwerdt. Ein System zur Transformation von Konsistenz in Anwendungsbedingungen. Berichte aus dem Department für Informatik 11/06, 114 pages, Universität Oldenburg, 2006.
[ .pdf ]

[HPR06]

Annegret Habel, Karl-Heinz Pennemann, and Arend Rensink. Weakest preconditions for high-level programs (long version). Berichte aus dem Department für Informatik 8/06, 35 pages, Universität Oldenburg, 2006.
[ .pdf ]