Curriculum vitae



6. 6. 1965 in Bad Honnef, Germany

marital status




Education and carreer


7. Feb. 07

Habilitation in Computer Science at the Faculty of Engineering, Christian-Albrechts-University, Kiel. Title of the habilitation thesis: Object-connectivity and observability for class-based, object-oriented languages. External reviewers Prof. Dr. Michael Mendler (University Bamberg) Prof. Dr. Gordon Plotkin (University Edinburgh), Dr. Frank de Boer (CWI Amsterdam), Prof. Dr. Davide Sangiorgi (University Bologna).

12. Nov. 98

Doctorate of Engineering (Dr.-Ing.) in Computer Science at the Technical Faculty, Friedrich-Alexander-University, Erlangen-Nürnberg. Title of the doctoral thesis: “Polarized Higher-Order Subtyping”. Evaluation “very good”. Date of submission: 8. January 1998, defended: 12. Nov. 1998. Reviewers: Prof. Dr. Horst Müller (University Erlangen-Nürnberg), Prof. Dr. Giorgio Ghelli (University Pisa).

31. March 92

Diploma in Computer Science (Dipl.-Inf. Univ.) at the Faculty of Engineering Sciences, Friedrich-Alexander-University, Erlangen-Nürnberg. Title of the diploma thesis : “Completeness of a proof system for Hennessy-Milner logic with recursion” (in German). Overall grade: 1.2 (very good “with distinction”), grade of the diploma thesis: 1.0 (“very good”).

Nov. 86 – March 92

Study of computer science (university diploma studies) at the Friedrich-Alexander-University, Erlangen-Nürnberg. minor subject: physics with focus solid state and quantum physics.

June 84

Abitur (German high school diploma)

Sept. 75 – Juli 77

Joseph-Hofmiller-Gymnasium in Freising

Sept. 77 – Juni 84

Rhön-Gymnasium Bad Neustadt a.d. Saale

Aug. 71 – Juli 75

Elementary schools in Lemgo, Suttrop, and Freising

    Positions held

since Aug. 06Feb. 06

senior researcher at the Institute of Computer Science of the University Olso, in the group “Precise Modelling and Analysis”. Project work, mainly in the EU project Credo, additionally teaching

Feb. 97 – Feb. 06

scientific assistant at the chair of Software Technology (Prof. Dr. de Roever) at the University Kiel. Various teaching obligations and collaboration in different international projects

April 94 – Jan. 97

Scientific assistant at the chair of Computer Networks and Communication Systems (Prof. Dr. Herzog) at the University Erlangen-Nürnberg. Employed at a project position, but with different teaching obligations, as well. Collaboration within different projects

winter term 90 –
winter term 92

student assistant, different tasks within the SFB sub-project “Specification and verification of distributed systems” (student tutor, project work)

winter term 88 –
winter term 89

student assistant for the lectures Logic and Recursion Theory I and II at the chair of Theoretical Computer Science

    Additional jobs

May 86 – Oct. 86

Work as non-medical aide at the district hospital Mellrichstadt

    Military resp. community service

Aug. 84 – März 86

Community service at the district hospital Mellrichstadt

Third-party funded projects

I participated scientifically in the following projects. In ABSolut, Credo, the Mobi-J-projects, the DAAD-ARC projects and the SFB sub-project I participated in writing the application and was resp. I am responsible for different tasks. I am project leader of the Norwegian side of the DAAD-NFR project. In the Vires-project I was responsible for different tasks but I did not participate in working out the application. In Omega I participated in the project but I was not responsible for a work package and did not participate in working out the application

from 2008 on?

“Automated validation for behavioral interfaces of asynchronous active objects”. 2-years bilateral collaboration between the Universty of Oslo and the University Kiel within the DAAD-NFR PPP programme of person exchange. The application is submitted and under review.

from 2008 on?

ABSolut: “Abstract Behavioural Specification and Analysis of Software Families”. Requested European project within the framework of FP7, programme “Cooperation”, theme “Information and Communication Technologies”, STREP-application, objective ICT-2007.1.2 “Service and software architectures, infrastructures & engineering”. The project consists of 6 academic and 3 industrial partners. The application is submitted and under review.

1. Sept. 06 – 31. Aug. 09

Credo: “Modeling and analysis of evolutionary structures for distributed services”. European project within the framework of FP6, priority 2, “Information Society Technologies”, call 5, activity IST-2005-2.5.5 Software and Services, project number IST-33826.

Academic partners: CWI, The Netherlands; University Oslo, Norway; CAU Kiel, Germany; TU Dresden, Germany; University Uppsala, Sweden; United Nations University, Macao, China. Industrial partners: Almende, The Netherlands; Rikshospitalet – Radiumhospitalet HF, Norway. Norsk Regnesentral, Norway.

2002 – 2004

European IST-2001-33522 project Omega: Correct Development of Real-Time Embedded System. Project partners: Verimag, University Grenoble, France; Centrum voor Wiskunde en Informatica, The Netherlands; Christian-Albrechts-Universität, Germany; University Nijmegen, The Netherlands; Weizmann Institute, Israel; Office, Germany. Industrielle partners; EADS SPACE Transportation, France; France Telecom R & D, France; Israeli Aircraft Industries, Israel; National Aerospace Laboratory, The Netherlands

15. Sept. 01 – 14. Sept. 04

MobiJ-I: “Assertional methods for mobile asynchronous channels Java”. Bilateral German-Dutch (DFG-NWO) project RO 1122/9-1, RO 1122/9-2. Partners: University Kiel; CWI, Amsterdam; LIACS, Leiden

15. April 05 – 14. April 08

MobiJ-II: “Formal Methods for Components and Objects”. Funded in the same way and with the same partners as MobiJ-I, RO 1122/9-4.

1. May 97 – 30. Apr. 00

European 4th Framework Esprit Project 23498 VIRES (Verifying Industrial Reactive Systems)

Academic project partners: University Eindhoven, The Netherland; Verimag, University Grenoble, France; CAU Kiel, Germany; University Liège, Belgium, Weizmann-Institute, Israel. Industrial partners: Intracom, Greece

Jan. 89 – Dec. 98

DFG Sonderforschungsbereich SFB 182 (Multi-processor- and network configurations), sub-project C2: “Spezification and verification of distributed systems”

July 95 — June 98

ARC exchange project: “Co-development of object-oriented programs in LEGO” (ARC is the Academic Research Council, a joint organization of the German Academic Exchange Organization (DAAD) and the British Council (BC)). Project partners: University Erlangen and LFCS, University Edinburgh.

Jan. 92 — Dec. 94

ARC exchange project: “ Mathematical foundations for the refinement of distributed systems”. Project partners: University Erlangen and LFCS, University Edinburgh.

Software projects

In most cases my research was and is motivated by practical problems resp. by theoretical questions with practical relevance. In the context of the project I participate(d), I was directly or indirectly involved in the practical development and application of tools as part of the project work program. In particular within the European projects, the software development tooks place, resp. takes place together with industrial partners. Besides the theoretical foundations, to which I contributed in the different projects, I participated in a couple of projects also directly to the software development, the programming, and the application of different analysis and verification tools.

in Teil des Projektes auf deutscher Seite war die Entwicklung eines “verification condition generators”, im wesentlichen eine Art Compiler, der annotierte Programme in zu beweisende Aussagen eines Theorembeweisers, in diesem Fall PVS, "ubersetzt. Im Rahmen des Projektes war ich an der Konzeption des Werkzeugs beteiligt. Die eigentliche Programmierung (in Java) wurde von Frau Ábrahám im Rahmen ihrer Doktorarbeit durchgef"uhrt. In der Doktorarbeit, verteidigt der Universit"at Leiden, fungierte ich als “co-promoter”.

n Zusammenarbeit mit der Universit"at Kiel entsteht in Mobij-II ein “black-box” Testwerkzeug f"ur speziell Java-Programme. Das Werkzeug basiert auf Beobachtungssemantiken, wie sie in MobiJ untersucht wurden und unter anderem in meiner Habilitationsschrift formalisiert sind.


Das Projekt beinhaltete umfangreiche eigene Werkzeugentwicklung (speziell von Modellpr"ufern) sowie die Modellierung und Validierung eines industriellen ATM-Protokolls.
  • – Ich war unter anderem verantwortlich (neben 2 anderen Projektpartnern) f"ur die Spezifikation und Modellierung der Fallstudie mit kommerziellen Modellierungswerkzeugen (basierend auf SDL). Ferner wendete ich Modellpr"ufer, speziell Spin, zur Verifikation und Validierung auf die Fallstudie an (in Kooperation mit haupts"achlich der TU Eindhoven und dem CWI, Amsterdam). Die Zusammenarbeit mit diesen Partnern f"uhrte zu einem Analysewerkzeug zur Linderung der Problems der Zustandsraumexplosion bei derartigen Protokollen.
  • – In einem weiteren Teilbereich des Projekts, f"ur dem ich (zusammen mit der TU Eindhoven und Verimag, Grenoble) verantwortlich war, entwickelte und implementierte ich ein Progamm zur automatischen, heuristischen Abstraktion basierend auf “Transducern” (in ocaml).

MobiJ I:


MobiJ II:



Auch das Arbeitsprogramm des Projektes, mit dem ich momentan haupts"achlich besch"aftigt bin, hat einen betr"achtlichen Teil Softwareentwicklung. Aufgaben, die in Oslo in Arbeit sind, umfassen die Entwicklung von Typsystemen, statischen Analysewerkzeugen und Compilern, aber auch Eclipse-Integration der Teiltools. Die Implementierungsarbeiten haben erst begonnen (Parser, Compiler) und sind teilweise (Typechecker) erst in der Konzeptionsphase als Teil des wissenschaftlichen Programms.


Wenn auch kein Softwareprojekt in industriellem Rahmen oder als Teil einen Forschungsprojektes, war die achtst"undige Veranstaltung “programming-in-the-many”, die ich wiederholt leitete, als gemeinsames Softwareprojekt konzipiert. An der umfangreichsten der Veranstaltungen (WS 98/99) nahmen "uber 30 Studenten teil, die alle an der gemeinsamen Aufgabe arbeiten, einschlie"slich der Ausarbeitung der Requirements, des Testens, der Integration, der Pr"asentation, etc. Nicht alle der Veranstaltungen waren so gut nachgefragt, doch war in jedem Fall eine ausreichende Anzahl von Studierenden interessiert, um das “in-the-many” zu rechtfertigen, und um die Probleme und Herausforderungen kollaborativer (Software-)Projektarbeit in der Lehre zu vermitteln.


    Research interests

type theoretical
foundations of OO:

My doctoral thesis was concerned with the type theoretic resp. proof theoretic fouXA0; Research interests

type theoretical
foundations of OO:

My doctoral thesis was concerned with the type theoretic resp. proof theoretic foundations of a functional calculus for object-oriented languages. In particular, I proved decidability of Fω (“F-Omega-Sub”), a higher-order λ-calculus which has been investigated as functional core calculus for object-oriented concepts and powerful enough to represent subtyping, inheritance, encapsulation, and late-binding. Based on a related functional encoding on object-oriented features, I worked also on the the formal verification of such programs with the help of theorem-provers, in particular in the constructive proof assistant Lego

Hoare logics
for multi-threaded
oo languages

In contrast to the functional and type-theoretical semantical theories I dealt with in my PhD thesis, I became interested in other important aspects of object-oriented programs such as state, in particular in the form of the heap, and concurrency in the form of multithreading. Besides that, the emphasis shifted to methods for the verification of object-oriented programs. Inspired by language features as found in Java, I worked in the MobiJ-project on the Hoare-style verification of multi-threaded Java-like programs.

observable behavior
of oo languages:

During the mentioned activities concerning the proof-theoretical account of aspects of multithreaded Java, I became interested in the observable, fully abstract behavior of class-based, object-oriented programs. Observational equivalence equates two program phrases when no context exists able to differentiate between them and is a fundamental question in the semantics of programming languages.

model checking:

Mainly in the context of the Vires-project, I did research on the verification of communication protocols based on model checking, i.e., the automatic state-exploration of the (model of the) protocol at hand. Motivated by a concrete case study given in SDL, a standardized protocol description language, the focus of that research had been to design theories, methods, and practical approaches to ameliorate the state explosion when modelling such protocols. In particular, as inspired by the case study, to get a grip on the state explosion entailed by the asynchronous, buffered nature of such protocols. All this work was in the context of the enumerative model checker Spin.


Besides the mentioned topics, I worked also on automata-theoretic results usable for parameterized model checking. A few papers are concerned with proof-systems for hybrid systems, a well-known formal model for systems combining discrete and continuous behavior, and furthermore strategies for bounded model checking linear hybrid systems. Further papers deal with abstraction, composition, and model checking for parameterized systems, the semantics and expressivity of modal transition systems, and type systems to ensure certain communication patterns in the π-calculus, the calculus of mobile channels.

    Projects and grants

SFB project

“Specification and verification of distributed systems” within the SFB-project 182, Erlangen


Esprit Project Vires

EU Project Credo

    Conference organization


(Distributed Computing Techniques): publicity chair and member of organizing commitee


IFIP WG 6.1 International Conference on Formal Methods for Object-Based Distributed Systems: steering commitee member since 2007
  • – Fmoods'08: programm commitee member
  • – Fmoods'07: programm commitee member and publicity chair
  • Fmoods'06: program commitee member and publicity chair
  • Fmoods'05: program chair
  • Fmoods'03: program commitee member


12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: program commitee member


International Conference on Intelligent Computer Communication and Processing, track static analysis and verification
  • ICCP'07: program commitee member
  • ICCP'06: program commitee member



I have been acting as reviewer for (amongst others) the following conferences: International Conference on Intelligent Computer Communication and Processing (ICCP '07, '06), Formal Aspects of Component Software (FACS'07), International Conference on Concurrency Theory (Concur '07, '01), IFIP International Conference on Formal Methods for Object-Based Distributed Systems (Fmoods '07, '06, '05, '03), 13th International Workshop on Expressiveness in Concurrency (Express'06), International Conference on Functional Programming (ICFP), International Workshop on Verification, Model Checking and Abstract Interpretation (VMCAI'02), Foundations of object-oriented languages/Workshop on Object-Oriented Development (Fool/Woods'06), Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), Formats-FTRTFT 2004, FSEN'07, Principles of programming languages (POPL'05), ATVA'07, Formal Methods (FM'06), FTRTFT, Programming Concepts and Methods (Procomet'98), Foundations of Software Technology and Theoretical Computer Science FSTTCS' 97, Logic in Computer Science (LICS 06, '95, '98, '99), Computer Aided Verification (CAV'04), European Conference on Object-Oriented Programming (ECOOP'99), FMCO'04, Formal Methods for Networked and Distributed Systems (Forte'07), International Colloquium on Automata, Languages and Programming (ICALP'05), Theoretical Aspects of Computer Science (STACS'97), Tools for System Design and Verification (Tools'02)


In addition, I reviewed contributions to the following international journals: Formal aspects of computing (FAC), Journal of Logic and Algebraic Programming (JLAP), Information and Computation (IC), Software and Systems Modelling (SoSym), Theoretical Computer Science (TCS), International Journal on Software Tools for Technology Transfer (STTT)



static analysis

master-level/Ph.D level lecture (2006)

algorithms &
data structures

undergraduate lecture for engineers with programming exercises (4 times)

theorem proving

graduate level lecture with exercises (2+2h)

semantics of
oo languages

graduate level lecture with extercises (2+2h)


in addition to the above lectures, which I designed and carried out on my own, I assisted also in the following lectures:
  • – operating systems (undergraduate level, 4 times)
  • – distributed algorithms (graduate level)
  • – Software specification techniques for distributed systems Statemate/SDL
  • – hybrid systems (graduate level)

    lab courses

embedded systems

programming Lego mindstorms robots with Esterel, a synchronous language (2 times)

Java programming

an introductory course at graduate level

software project

undergraduate level software project using Java

software engineering

an introductory course at undergraduate level course for engineers (2 times)


an 8 hourse graduate level software project of collaborative design and programming (8h, 5 times with varying topics)


  • – the Universal Modelling Lanuage (UML)
  • – model checking (2 times)
  • – semantics and verification of object-oriented programs
  • – hardware verification
  • – compositional verification of distributed programs
  • – component based software engineering
  • – distributed algorithms (4 times)
  • – distributed and concurrent programming
  • – grid computing


open door

I gave presentations and demos for the general public on the occasions of the University's “open door days”. Besides that I gave presentations advertizing the academic subject of computer science for high school students a couple of times.

CS prep course

when the University Kiel established an introductory week-long preparatory course as service for beginners of computer science or of other subjects with computer interest, I was active in working out part of the program and I presented it at the beginning of each winter semester (4 times).

further duties

Apart from my more theoretical scientific inclinations, I was always involved in Erlangen as well as in Kiel in administrative tasks. In Erlangen, I was responsible for installing and maintaining part of the local software at the chair. Similarly in Kiel, where, among other software, I helped maintaining Java and related software for the computer science department. Also I was responsible for the web-pages of the chair of Software Engineering.





I am fluent in German and English. In addition, I speak —in varying degrees of imperfection— Norwegian, French, Spanish, and Italian

This document was translated from LATEX by HEVEA.