Formal Languages

Dr. Karl-Heinz Pennemann

Address: Dr. Karl-Heinz Pennemann
University of Oldenburg
Faculty II
Department of Computing Science
D-26111 Oldenburg
Germany
Foto
Room: A2 2-209
Phone: +49 441 798-2978
Fax: +49 441 798-2965
email: K.H.Pennemann

 


top of page

Curriculum Vitae

09/2009 Defense of the PhD thesis "Development of Correct Graph Transformation Systems" (summa cum laude)
07/2008 - 12/2005 PhD student and scholarship holder at the DFG graduate school TrustSoft (Trustworthy Software Systems)
08/2005 - 10/2004 Research associate with teaching duties; Formal Languages Group of Prof. Habel, University of Oldenburg
09/2004 Diploma (MSc.) degree (with honors) in Computer Science
09/2004 - 10/1997 Studies of Computer Science at the University of Oldenburg
06/1997 A-Level (Abitur), Fachgymnasium Wirtschaft, Papenburg (Grammar School for Business Education)
10/1977 Born in Papenburg, Germany


top of page

Research

In my PhD thesis, I investigate methods for the verification of graph-based program specifications.

Overview

My research interest include automated deduction (theorem proving); semantics, specification, and verification of programs; reactive systems; systematic development and automatic synthesis of correct programs; and automatic and machine-supported verification tools.


top of page

Projects


top of page

Research visits

  • May 2006: Visit of the Formal Methods and Tools Group, University of Twente, The Netherlands following the invitation of Prof. Dr. Arend Rensink.

top of page

Talks

  • January 2007: Talk at the Graph Transformation Day of the University Bremen. Host Prof. Dr. Hans Jörg Kreowski. Titel "Weakest Preconditions for High-Level Programs".
  • November 2006: Talk at the International Research Training Groups Workshop 2006, Schloss Dagstuhl, Wadern. Host Prof. Dr. Willi Hasselbring. Titel "Development of Correct Graph Transformation Systems".
  • May 2006: Talk at the seminar of the Formal Methods and Tools Group, University of Twente, The Netherlands. Host Prof. Dr. Arend Rensink. Titel "Weakest Preconditions for High-Level Programs".
  • Presentations at international conferences and workshops, e.g., in Natal, Brazil (2006); Lisbon, Portugal (2007); and Leicester, UK (2008).

top of page

Publications

[Pen09]
Karl-Heinz Pennemann. Development of Correct Graph Transformation Systems. PhD thesis, Department für Informatik, Universität Oldenburg, Oldenburg, 2009. Electronic Dissertation. [ bib | .pdf ]
[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. [ bib | .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. [ bib | .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. [ bib | .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. [ bib | .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. [ bib | .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. [ bib | .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. [ bib | .pdf ]
[HPR06b]
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. [ bib | .pdf ]
[HPR06a]
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. [ bib | .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. [ bib | .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. [ bib | .ps.gz ]
[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. [ bib | .ps.gz ]
[EEHP04]
Hartmut Ehrig, Karsten Ehrig, Annegret Habel, and Karl-Heinz Pennemann. Constraints and application conditions: From graphs to high-level structures. In Graph Transformation (ICGT'04), volume 3256 of Lecture Notes in Computer Science, pages 287-303. Springer-Verlag, 2004. SpringerLink. [ bib | .ps.gz ]
[Pen04]
Karl-Heinz Pennemann. Generalized constraints and application conditions for graph transformation systems. Master's thesis, Dept. of Computing Science, University of Oldenburg, Oldenburg, 2004. [ bib | .pdf ]
[EMQP04]
Marco Eissen, Radoslaw Mazur, Heinz-Georg Quebbemann, and Karl-Heinz Pennemann. Atom economy and yield of synthesis sequences. Helvetica Chimica Acta, 87:524-535, 2004. [ bib | http ]

top of page

Theses

[Pen09]
Karl-Heinz Pennemann. Development of Correct Graph Transformation Systems. PhD thesis, Department of Computing Science, University of Oldenburg, Oldenburg, 2009. Electronic Dissertation.
[ bib | .pdf ]

[Pen04]
Karl-Heinz Pennemann. Generalized constraints and application conditions for graph transformation systems. Master's thesis, Dept. of Computing Science, University of Oldenburg, Oldenburg, 2004.
[ bib ]