Formal Languages

Development of Correct Graph Transformation Systems

 

go next top of page

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.

 

go next top of page go back

2 References

go next top of page go back

2.1 Journal publications

[HP09]
Annegret Habel and Karl-Heinz Pennemann. Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science, 19:1-52, 2009. MSCS-Link. [ .pdf ]
[EHPP06]
Hartmut Ehrig, Annegret Habel, Julia Padberg, and Ulrike Prange. Adhesive high-level replacement systems: A new categorical framework for graph transformation. Fundamenta Informaticae, 74:1-29, 2006. [ .pdf ]
[EEHP06]
Hartmut Ehrig, Karsten Ehrig, Annegret Habel, and Karl-Heinz Pennemann. Theory of constraints and application conditions: From graphs to high-level structures. Fundamenta Informaticae, 74(1):135-166, 2006. [ .ps.gz ]

go next top of page go back

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 ]
[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. SpringerLink. [ .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. SpringerLink. [ .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. SpringerLink. [ .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), volume 10, pages 249-262. Electronic Communications of the EASST, 2008. ECEASST-Link. [ .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 the EASST, 2007. ECEASST-Link. [ .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. SpringerLink. [ .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. SpringerLink. [ .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. SpringerLink. [ .ps.gz ]

go next top of page go back

2.3 Further publications

[Ble08]
Christian Bley. Ein Editor zum Erstellen von Graphprogrammen. Technical report, 2008. [ .pdf ]
[MH08]
Mohamed Mosbah and Annegret Habel. Workshop on graph computation models, 2008. SpringerLink. [ .pdf ]
[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 ]
 top of page go back