A large part of my work is devoted to the development of Averest, a framework for the specification, verification, and implementation of embedded systems. In particular, I have implemented a symbolic model checker and a tool for hardware/software synthesis. The model checker can be used for verifying finite as well as infinite state systems at various levels of abstraction. Besides widely used global (fixpoint based) model checking algorithms, it also supports local (tableaux based) model checking algorithms and bounded variants thereof. For more information, please see the overview of the Averest project.
I am also involved in the project "Verification of Adaptive Systems (EVAS)" which is part of the excellence cluster "Dependable Adaptive Systems and Mathematical Modeling (DASMOD)". The goal of the project is the development of new methods for modeling, analysis, and model-based synthesis of embedded systems that support dynamic adaptivity. Adaptation is particularly important in safety-critical embedded systems to cope with changing environmental conditions and to provide a maximum degree of dependability. A central topic of the project is the integration of modeling and verification techniques for adaptive systems.
Teaching
Courses
Verification of reactive systems, University of Kaiserslautern, winter term 2007/2008
Parallel computers, University of Kaiserslautern, summer term 2007
Computer systems II, University of Kaiserslautern, winter term 2005/2006
Computer systems, University of Kaiserslautern, winter terms 2002/2003, 2003/2004, 2004/2005
Foundations of digital technology II, University of Kaiserslautern, summer term 2003
Computation structures, University of Karlsruhe, summer terms 2000, 2001, 2002
Graduate seminar, University of Karlsruhe, summer terms 2000, 2001, 2002 and winter terms 2000/2001, 2001/2002
Theses
Christoph Wagner. Automatenbasierte Entscheidungsverfahren für Presburger-Arithmetik. Diploma thesis, University of Kaiserslautern, 2006
Daniel Baudisch. Implementierung und Verifikation eines RISC-Prozessors. Project thesis, University of Kaiserslautern, 2006
Christoph Wagner. Evaluierung von Algorithmen zur Berechnung fairer Pfade. Project thesis, University of Kaiserslautern, 2005
Mareike Schmidt. An Algorithm for Restriction of Finite Automata. Diploma thesis, University of Kaiserslautern, 2005
Mareike Schmidt. Bounded Local Model Checking. Project thesis, University of Kaiserslautern, 2004
Johann Weber. Entwurf eines RISC-Prozessors mit synchronen Sprachen. Diploma thesis, University of Kaiserslautern, 2004
Karl-Christian Pammer. Minimierung endlicher Automaten mit großen Alphabeten. Project thesis, University of Kaiserslautern, 2004
Seminars
Current processor technologies, University of Kaiserslautern, summer term 2006
Verification of reactive systems, University of Kaiserslautern, winter term 2003/2004
Normal forms for propositional logic and their application in system design, University of Kaiserslautern, winter term 2002/2003
Low power design, University of Karlsruhe, summer term 2000
Tutorials and Workshops
Design and Verification of Reactive Systems, International workshop for foreign students, University of Kaiserslautern, July 4, 2006
Tutorial on reactive systems design, University of Kaiserslautern, July 17, 2006
Organization of the 16th International Workshop on Trends and Topics in VLSI, See, Austria, 2002
Fun
"Birne sucht einen Fehler" was one of my favorite stories when I was a child and certainly influenced the choice of my profession... (The story is about an electric bulb that searches a bug in a mainframe computer. However, at that time I did not yet know anything about verification.)
