M. Oliver Möller, Ph.D.
Nürnberger Straße 5
28215 Bremen
Tel.: [private]+49 421 - 247 5656
[mobile]+49 179 – 326 74 32


compiled:  November 19, 2006

Curriculum Vitae

Personal Information

born on June 7, 1972 in Burgau, Germany


German citizen

Professional Activities


Employed as project leader at Verified Systems Internatioal GmbH


(www.verified.de). Activities include:




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


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



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



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



University of Pennsylvania (UPenn), Philadelphia, USA


research group Rajeev Alur,



design and implementation of heuristic structuring algorithms for the model-checker Mocha



University of Aarhus, instructor in the undergrad course “Fundamentale Modeller” (automata theory and formal languages), taught by Prof. Flemming Nielson



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.



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



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


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



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)




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