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:
Some development tools I have used in a professional context:
Operating Systems:
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