|
|
|||||||||||
|
|
|||||||||||
compiled: November 19, 2006
Curriculum Vitae
Personal Information
born on June 7, 1972 in Burgau, Germany |
German citizen |
Professional Activities
9/2002–today | Employed as project leader at Verified Systems Internatioal GmbH |
| (www.verified.de). Activities include: |
| Tool-Development, |
| Performing system- and error-anaylsis, |
| Contruction and maintainance of test-beds, |
| Preparation and performing training courses on tool and tool-environment usage |
| tool support (mail and phone) |
| 2004 onward: in the function of a quality manager (ISO-9001 certified company): |
| process devoloment, documentation, assesment, planning and performing of quality audits |
12/2000-12/2001 | European Project No. IST-1999-10069, “Advanced Information Technology-Workshop for Object Oriented Design and Development of Embedded Systems” (AIT-WOODDES), responsible person for scientific partner Aalborg University, |
| collaboration on the UML profile for Real-Time Modeling, integration of various verification techniques is the object-oriented design process ROPES |
7/2001-8/2001 | Stanford Research Institute SRI International, Menlo Park, USA |
| research group John Rushby, |
| development of an abstraction-based framework for the verification of real-time systems |
9/2000-2/2001 | Uppsala University, Sweden, research group Wang Yi |
| design of an hierarchical modeling language for real-time systems, XML representation, design and reference implementation of a translation mechanism catering for the real-time model-checker Uppaal |
4/2001-6/2001 and 4/2000-6/2000 | Århus/Aalborg University: instructor Ph.D.-level course “Verification”, taught by Kim G. Larsen; responsible for applied verification tools |
9/1999-11/1999 | University of Pennsylvania (UPenn), Philadelphia, USA |
| research group Rajeev Alur, |
| design and implementation of heuristic structuring algorithms for the model-checker Mocha |
2/1999-6/1999 | University of Aarhus, instructor in the undergrad course “Fundamentale Modeller” (automata theory and formal languages), taught by Prof. Flemming Nielson |
10/1997-2/1998 | University of Ulm, department for artificial intelligence |
and 10/1996-2/1997 | teaching assistant in the undergrad course “Grundlagen der Künstlichen Intelligenz” (introduction to artificial intelligence), taught by Prof. Friedrich von Henke et.al. |
9/1996-10/1996 | Stanford Research Institute SRI International, Menlo Park, USA |
| research group John Rushby, |
| design and implementation of decision procedures for bit-vectors in the automated theorem prover PVS, based on preliminary work in Ulm on this topic |
9/1995-2/1996 | University of Ulm, department for artificial intelligence, research assistant, |
| modeling of the language Occam in the theorem prover PVS |
IT Skills
hands-on programming experience with Java, C (very good), C++ (good), Lisp (very good), Assembler (good), SML (good), and Prolog (basic) |
extensive user-experience with different tools for formal verification, in particular Uppaal (expert), Mocha (very good), PVS (good), CWB (good), SPIN (good), and Otter (basic) |
very good developer experience as part of the project team of the tools Uppaal, Mocha, and PVS (Java/C++/Common Lisp) |
comprehensive expericience in using syntax-analysis tools like lexer/parser pairs (flex/yac, javacc) |
good understanding of object-oriented design methodologies and the unified modeling language (UML) |
familiarity with common sofware engineering tools, including configuration management (CVS, SVN, ClearCase) and failure tracking (ClearQuest, GNATS) familiarity with scripting languages like Perl and Awk, experienced in programming Makefiles |
good understanding of the operating systems UNIX/Linux, experienced in bash shell programming |
thorough user-experience with MS Windows-based applications, MS Word; familiar with Staroffice and Acrobat Reader |
basic understanding of web-publishing, HTML, XML, and Javascript |
exhaustive user-experience with the text-processor LATEX and the graphical editor xfig |
daily use of the editor Emacs, good experience with programming of extentions (emacs lisp) |
Additional Skills
language skills: German (mother tongue), technical English (fluent), Danish (good) |
thorough experience in the presentation of technical material, due to numerous talks given in international conferences |
routine in organization and planning, partially due to frequent external stays in connection with research projects and personal vacation tours |
familiar in preparation and moderation of discussions, due to years of voluntary work for the German scout organization DPSG as troop leader, chapter manager, member of organization teams on district and diocese level, |
preparation and conduction of leader educations, working with the project method |
Areas of Expertise
formal methods: modeling and specification, mathematical foundations, abstraction techniques |
algorithmic verification: decision procedures, model-checking, automated theorem-proving, special cases and common optimizations, approximation techniques |
symbolic data-structures: binary decision diagrams (BDDs), zone-based representation of real-time via difference bounded matrices (DBMs) and clock decision diagrams (CDDs) |
logic: Kripke-structures, temporal logics, branching-time and linear-time operators |
complexity theory: decidability, hard problems, NP-completeness, formal languages, automata theory, classification of real-time systems |
Higher Education and Degrees
May 7, 2002 | Ph.D. degree in science, University of Aarhus, Denmark |
7/1998-5/2002 | BRICS international PhD school, Århus, Denmark |
| applied there based on BRICS’ reputation in education and research |
| supervisor: Kim G. Larsen (Aalborg University) |
| main topics: verification, formal methods, real-time systems |
| participation in international conferences and presentation of research results, member of the Uppaal project team |
| thesis: “Structure and Hierarchy in Real-Time Systems” (English) |
March 12, 1998 | Diplom-Informatiker, Universität Ulm, rated “sehr gut” (top marks) |
| corresponds to a master in computer science |
10/1992-3/1998 | University of Ulm, student of Informatik (computer science major) |
| minor: first chemistry, then mathematics (changed because of its exactness) |
| main topics: artificial intelligence, automated theorem proving |
| master thesis “Solving Bit-Vector Equations – A Decision Procedure for Hardware Verification” (English) |
School/Service
8/1991-10/1992 | Therapiezentrum Burgau, nursing hospital work (instead of serving in the Germany Army) |
July 10, 1991 | Abitur, Dossenberger Gymnasium Günzburg (Bavaria), rated 1.0 |
| (top mark) |
Personal Activities, Hobbies
outdoor: walking tours, hiking, and trekking |
scout activities: co-organization of weekend programs, camps, and leader education courses |
motor bike cruising |
smaller programming projects (I’m part of the C64-generation), Java applets, scripts, micro-controller (e.g., the control unit of a theater light mixer) |
film and film history, movie classics |
writing of amateur story-books in a team of authors, topics generally satirical or humoristic; current long-term project is a criminal comedy |
