I am a professor of formal methods in computer science at the Munich University of Applied Sciences. My teaching includes program verification, compilers, cryptography and theoretical computer science.

From October 2018 to March 2020 I worked as a formal methods software engineer at Input/Output Hong Kong on formal specification and verification of distributed ledger technologies. From June 2016 to September 2018 I was working as research engineer at Diffblue in the area of automated test generation and formal analysis of software for embedded systems. An important tool for this is CPROVER/CBMC. From October 2012 to April 2015 I was a Software and systems engineer in the modeling and proof group at Systerel in Aix-en-Provence (France). For rail interlocking systems, I developed model transformations from graphical models to input specifications of formal analysis tools (Systerel Smart Solver). I used the Event-B formalism to support systems engineering of critical systems in aerospace, formal data validation for SIL 4 railway applications and I participate in the openETCS European research project using formal verification for system development and SCADE for the implementation of a ETCS sub-system.

I studied Applied Computer Sciences and Mathematics at the University of Augsburg. In 2005 I finished my diploma thesis on multi-criteria optimization of automated mixed palletizing algorithms in cooperation with KUKA SysTec (now part of KUKA AG). From 2005 to 2009 worked as a researcher at the University of Augsburg. From 2009 to 2011 I worked as a researcher at the Otto-von-Guericke University of Magdeburg, where I finished my PhD in safety analysis using formal methods. In September 2012 I received the Software Engineering award of the Ernst Denert Foundation for my PhD thesis. From October 2011 to October 2012 I worked as a Post-Doc researcher in the CONVECS group at INRIA Rhône-Alpes in Grenoble.

Besides research, I taught university courses in industrial robot programming, Java smartcards programming, cryptographic protocols and mathematical logic. In several seminars and university courses we used the SCADE suite as academic partner of Esterel Technologies. I also supervised several Bachelor, Master and Diploma theses, both directly at the university and in cooperation with companies like KUKA AG or Infineon Technologies.

My main interest is to use formal methods and mathematics to provide correct and efficient solutions for real-world problems, in particular for critical systems. I am very interested in declarative functional and logic based programming languages, as well as in computer security, in particular cryptographic algorithms, protocols and their correct implementation.

I was working on the software model-checker CBMC/JBMC and proprietary extensions
thereof for automatic test generation. Our work on the hardware model-checker
EBMC resulted in a publication at the DATE 2018 conference, winning the best
paper award in the *Design* track.

At Systerel I participated in the openETCS project with the goal of a common standard for railway signalization in Europe. In this project, a reference implementation will be developed which will be validated and verified using the open proof approach. Using Rodin I to developed an Event-B model for formal verification on the system level. Within a purely industrial context, I am working with the OVADO tool for formal data validation for safety critical systems. In both areas the work is done SIL 4 compliant according the standard CENELEC EN 50128. For another project I develop an Event-B model of a safety critical system in the aerospace domain to support systems engineering.

At Inria, I was working on the formal verification of choreography specifications (e.g., BPMN 2.0), implemented via distributed systems with asynchronous communication. For this I used the CADP toolbox, which is developed in the CONVECS (formerly VASY) group at INRIA Rhône-Alpes. I developed software to encode choreographies in LOTOS NT, analyze them for properties like realizability and, if necessary, interpret CADP counterexamples. This identifies all problematic messages in a choreography, and using additional synchronization messages, proposes a solution which enforces realizability. I have implemented the approach in Python to automatize is completely. My work resulted in publications at ATVA 2012 and FASE 2013.

For my PhD thesis I developed a method for a combined quantitative and qualitative model-based safety analysis, using model-checking tools like PRISM, MRMC and NuSMV. I implemented an appropriate modeling language using the ANTlr toolkit and the necessary model transformations in Common Lisp. I also worked on the integration of model-based safety analysis into the SCADE suite. My work on resulted in more than 16 publications, most notably at SAFECOMP (2007 and 2011), PRDC (2011), HASE (2010 and 2012) and in the Journal of Systems and Software (2013). My work is also the basis for the DFG-founded research project Probabilistic Models for Safety Analysis (ProMoSA), and is continued at Magdeburg by two PhD students.

In my diploma thesis I applied mathematical optimization to tune mixed palletizing algorithms for industrial robots to produce a minimal number of maximally stable pallets from a set of goods. The implementation was done in C# and comprised highly optimized mathematical algorithms, in particular for estimation techniques to reduce the number of (very costly) objective function calls. The simulation environment which I developed was in internal use at KUKA SysTec for several years afterwards.

**flycheck-mercury** This is an extension to Flycheck which allows on-the-fly syntax
checks for mercury programs in emacs. It can be found on github and can be
installed in Emacs24 via MELPA.

**Choreography Monitor (choreomon)** This software analyzes specifications of
choreographies with the CADP toolbox. It decides whether a choreography is
realizable. If this is not the case, the counterexamples provided by CADP are
exploited to add synchronization messages to the choreography. It is realized in
Python, the approach is described in our ATVA12 paper.

**Verification of Choreographies (verchor)** This software provides a generic format
for different choreography specifications (e.g., BPMN 2.0, conversation
protocols) based on XML. Models are validated using XSD and are transformed to
Lotos NT specifications for analysis with the CADP toolbox. The software has
been integrated into Eclipse.

**Safety Analysis and Modeling Language (SAML)** This language is an extension of
the PRISM modeling language. It allows to model Markov Decision Processes and is
especially suited for modeling safety critical systems. SAML models are
transformed for different model checkers, e.g., PRISM, MRMC, NuSMV or Cadence
SMV, depending on the nature of the properties to verify. The transformations
are proven to preserve the semantics of the models. The toolchain is realized
using ANTlr, Java and Common Lisp.

**Genetic Optimization with Kriging and Evolutionary Learning (GOKEL)** This
software provides a generic interface for multi-objective optimization
algorithms. I implemented the algorithms NSGA-2, ParEGO and OEGADO to optimize
automated palletizing algorithms for stability of pallets, packing density and
pallet numbers. It is realized in C#, provides a GUI, an objective function
interface and allows to specify the allowed time for optimization.

**Public Key Cryptography Prototype** For an university seminar on computer
security, I created a Haskell implementation of the basic functions to use RSA,
El-Gamal and El-Gamal on elliptic curves (Menezes-Vanstone) to encrypt and
decrypt string messages.

A short list of my talks in addition to the presentations of my articles at conferences:

Efficient Verification of Multi-Property Designs at Verification Futures 2018, Reading UK, June 14th 2018

**Industrial Formal Methods** in Trièves at the annual seminar of the CONVECS
research team of Inria Rhône-Alpes, 23-25 June 2014

Event-B for Safety Analysis of Critical Systems in Toulouse at the Rodin Workshop, 2-3 June 2014

openETCS Benchmark Model in Event-B / Rodin presented in Munich at Deutsche Bahn for the openETCS workshop, April 2013

**Verification of Interaction Based Systems** presented in Grenoble at Schneider
Electric, May 2012

**Quantitative and Qualitative Model-Based Safety Analysis** presented in Toulouse
at ONERA for the Model-Based Safety Assessment Workshop, March 2011

Computer languages that I have used in a professional context include:

- C++
- Haskell
- C#
- Java
- first order logic (B language notation)
- Common Lisp
- C
- Python
- JavaScript

Some development tools I have used in a professional context:

- emacs
- Eclipse
- Visual Studio
- git / svn / hg
- Rodin
- OVADO

Operating Systems:

- Linux
- OpenBSD
- Windows

Flexible Formality: Practical Experience with Agile Formal Methods Philipp Kant,
Kevin Hammond, Duncan Coutts, James Chapman, Nicholas Clarke, Jared Corduan,
Neil Davies, Javier Díaz, Matthias Güdemann, Wolfgang Jeltsch, Marcin
Szamotulski, Polina Vinogradova, *Trends in Functional Programming (TFP 2020)*,
2020

**Efficient Verification of Multi-Property Designs (The Benefit of Wrong
Assumptions)** Eugene Goldberg, Matthias Güdemann, Daniel Kroening & Rajdeep
Mukherjee, *Design Automation and Test in Europe (DATE 2018)*, 2018, **best paper award**

Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015 Manuel Núñez & Matthias Güdemann, Springer LNCS, 2015

Formal Verification of Industrial Critical Software Marielle Petit-Doche,
Nicolas Breton, Roméo Courbis, Yoann Fonteneau & Matthias Güdemann, *Proceedings
of the 20th Workhop on Formal Methods in Industrial Critical Systems (FMICS
2015)*, 2015

VerChor: A Framework for the Design and Verification of Choreographies
Matthias Güdemann, Pascal Poizat, Gwen Salaün & Lina Ye, *IEEE Transactions on
Services Computing (TSC)*, *accepted 1st March 2015*

Efficient optimization of large probabilistic models Simon Struck, Matthias
Güdemann & Frank Ortmeier, *Journal of Systems and Software*, Elsevier, 2013

VerChor: A Framework for Verifying Choreographies Matthias Güdemann, Pascal
Poizat, Gwen Salaün & Alexandre Dumont, *Proceedings of the 16th International
Conference on Fundamental Approaches to Software Engineering (FASE 2013)*, 2013

Multi-Objective Optimization of Formal Specifications Simon Struck, Matthias
Güdemann, Michael Lipaczewski & Frank Ortmeier, *Proceedings of the 14th High
Assurance System Engineering Symposium (HASE 2012) IEEE*, 2012

Counterexample Guided Synthesis of Monitors for Realizability Enforcement
Matthias Güdemann, Gwen Salaün, Meriem Ouederni, *Proceedings of Automated
Technology for Verification and Analyis (ATVA 2012)*, 2012

Trajectory Description Conception for Industrial Robots Sergey Alatartsev,
Matthias Güdemann, Frank Ortmeier, *Proceedings of the 7th German Conference on
Robotics (ROBOTIK)*, 2012

The ForMoSA Approach to Qualitative and Quantitative Model-Based Safety Analysis
Axel Habermaier, Matthias Güdemann, Frank Ortmeier, Wolfgang Reif & Gerhard
Schellhorn, *Railway Safety, Reliability and Security: Technologies and System
Engineering*, IGI Global, 2012

Unifying Probabilistic and Traditional Formal Model-Based Analysis Matthias
Güdemann, Michael Lipaczewski, Simon Struck & Frank Ortmeier, *Proceedings of
8. Dagstuhl-Workshop on Model-Based Development of Embedded Systems (MBEES)*,
2012

Qualitative and Quantitative Formal Model-Based Safety Analysis Matthias
Güdemann *PhD Thesis*, 2011

**Model-Based Multi-Objective Safety Optimization** Matthias Güdemann & Frank
Ortmeier, *Proceedings of the 30th International Conference on Computer Safety,
Reliability and Security (SAFECOMP 2011)*, Springer LNCS, 2011

**Towards Model-driven Safety Analysis** Matthias Güdemann & Frank Ortmeier,
*Proceedings of the 3rd international Workshop on Dependable Control of Discrete
Systems (DCDS 11),* IEEE, 2011

**Tool Supported Model-Based Safety Analysis and Optimization** Matthias Güdemann,
Michael Lipaczewski & Frank Ortmeier, *Proceedings of the 17th IEEE Pacific Rim
International Symposium on Dependable Computing (PRDC 2011)*, 2011

**Towards Making Dependability Visual - Combining Model-Based Design and Virtual
Realities** Frank Ortmeier, Matthias Güdemann, Michael Lipaczewski, Marco Schumann
& Robert Eschbach, *Proceedings of the 17th IEEE Pacific Rim International
Symposium on Dependable Computing (PRDC 2011)*, 2011

**Practical Experiences in Model-Based Safety Analysis** Frank Ortmeier, Michael
Lipaczewski & Matthias Güdemann, *Proceedings of the 2nd International Workshop
on Digital Engineering (IWDE)*, 2011

**A Framework for Qualitative and Quantitative Model-Based Safety Analysis**
Matthias Güdemann & Frank Ortmeier, *Proceedings of the 12th High Assurance
System Engineering Symposium (HASE 2010)*, IEEE, 2010

**Probabilistic Model-Based Safety Analysis** Matthias Güdemann & Frank Ortmeier,
*Proceedings of the 8th Workshop on Quantitative Aspects of Programming Languages
(QAPL 2010)*, ENTCS, 2010

**Quantitative Model-Based Safety Analysis: A Case Study** Matthias Güdemann & Frank
Ortmeier, *Proceedings of 5th conference for Sicherheit, Schutz und
Zuverlaessigkeit (SICHERHEIT 10)*, Lecture Notes in Informatics (LNI), 2010

**SysML in Digital Engineering** Matthias Güdemann, Stefan Kegel, Frank Ortmeier,
Olaf Poenicke & Klaus Richter, *Proceedings of 1st International Workshop on
Digital Engineering (IWDE)*, ACM, 2010

**ProMoSA - Probabilistic Models for Safety Analysis** Frank Ortmeier & Matthias
Güdemann, *Proceedings of 6th Dagstuhl-Workshop MBEES 2010: Model-Based
Development of Embedded Systems*, 2010

**A specification and construction paradigm for Organic Computing systems** Matthias
Güdemann, Florian Nafz, Frank Ortmeier, Hella Seebach & Wolfgang Reif,
*Proceedings of the 2nd IEEE International Conference on Self-Adaptive and
Self-Organizing Systems*, pages 233-242, IEEE, 2010

**Computing Ordered Minimal Critical Sets** Matthias Güdemann, Frank Ortmeier &
Wolfgang Reif, *Proceedings of the 7th Symposium on Formal Methods for Automation
and Safety in Railway and Automotive Systems (FORMS/FORMAT 08)*, 2008

**Developing Safety-critical Mechatronical Systems**
Matthias Güdemann, Frank Ortmeier & Wolfgang Reif,
*Self-optimizing Mechatronic Systems: Design the Future,* HNI-Verlagsschriftenreihe, 2008

**Modeling of self-adaptive systems with SCADE** Matthias Güdemann, Andreas Angerer,
Frank Ortmeier & Wolfgang Reif, *Proceedings of the 40th IEEE International
Symposium on Circuits and Systems (ISCAS)*, IEEE, 2007

**Using Deductive Cause Consequence Analysis (DCCA) with SCADE** Matthias Güdemann,
Frank Ortmeier & Wolfgang Reif, *Proceedings of SAFECOMP 2007*, Springer LNCS,
2007

**Formal Failure Models** Frank Ortmeier, Matthias Güdemann & Wolfgang Reif,
*Proceedings of the 1st IFAC Workshop on Dependable Control of Discrete Systems
(DCDS 07)*, Elsevier, 2007

**Towards Safe and Secure Organic Computing Applications** Matthias Güdemann,
Florian Nafz, Wolfgang Reif & Hella Seebach, *INFORMATIK 2006 — Informatik für
Menschen*, pages 153-160 Bonn, Germany, Köllen Verlag, 2006

**Formal Modeling and Verification of Systems with Self-x Properties** Matthias
Güdemann, Frank Ortmeier & Wolfgang Reif, *Proceedings of the 3rd International
Conference on Autonomic and Trusted Computing (ATC-06)*, Springer LNCS, 2006

**Safety and Dependability Analysis of Self-Adaptive Systems** Matthias Güdemann,
Frank Ortmeier & Wolfgang Reif, *Proceedings of the 2nd International Symposium
on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA
06)*, IEEE, 2006