Peter Lammich

Technische Universität München
Institut für Informatik
Boltzmannstr. 3
85748 Garching
Telephone: +49 (89) 289-17326
Telefax: +49 (89) 289-17307
Office: MI 00.09.065

From August 2017 to February 2018, I am research assistant professor at Virginia Tech.
For TUM-Students: You can still contact me by mail!
For VT-Students: Homepage at VT

I am a researcher (post-doc) at the chair for logic and verification of Prof. Tobias Nipkow.
My main research interest is the production of verified software by a top-down refinement process. For this, I'm using the theorem prover Isabelle/HOL, for which I have developed the Isabelle Refinement Framework and the Isabelle Collection Framework.
Other research interests include the automatic analysis of models for concurrent programs, and the mechanical verification of the analysis algorithms. To this end, I have explored dynamic pushdown networks, a model for concurrent programs with thread creation and locks as synchronization primitive. Moreover, we have developed the fully verified CAVA LTL model checker.
Recently, I have also worked on modeling web-services in Isabelle/HOL, and formally verifying their information flow security properties. As a demonstrator, we have developed the conference management system CoCon, that has formally verified information flow properties.


2001 - 2006
Study of computer science with electrical engineering as minor subject at the university of Dortmund
2006 - 2011
Dissertation at the University of Münster, supervised by Prof. Dr. Markus Müller-Olm.
2011 - ...
Member of the Theorem Proving Group of Prof. Tobias Nipkow at the TU München
8/2017 - 2/2018
Visiting Virginia Tech as research assistant professor in the group of Binoy Ravindran


See DBLP for a complete list


Refinement Framework

Verified Model-Checkers

Verified Security

Dynamic Pushdown Networks



Unpublished Isabelle/HOL projects.



Certified Programming (at Virginia Tech)
Lecture: Automata II: Tree Automata
Proseminar: SAT-Solvers - Theory, Tools and Applications
WS14/15, WS16/17
Program Optimization
Semantics of Programming Languages

Tutorials of Lectures

To be updated.
Tutorial of Einführung i.d. Theoretische Informatik
Tutorial of Semantics of Programming Languages
Tutorial of Equational Logic
Tutorial of Semantics of Programming Languages
Tutorial of Equational Logic
Tutorial of Semantics of Programming Languages

In Münster

I did teaching on various topics in Münster from 2006 to 2011. See the teaching page of Prof. Müller-Olm's group for details

from 2006 to 2011
Tutorials on Software Engineering, Theorie der Programmierung, and Model Checking
from 2006 to 2011
Software Praktikum
from 2006 to 2011
Seminars about Petri nets, theorem provers, and theory of programming

Student Projects and Theses

To be updated.
2014, with Nipkow, Esparza
Julian Brunner: Implementation and Verification of Partial Order Reduction for On-The-Fly Model Checking (Master Thesis)
2013, with Andrei Popescu
Sudeep Kanav: A secure web interface for a verified conference management system (Individual research project)
Julian Brunner, Manuel Eberl: Verified Conversion between NFAs and Regular Expressions (Praktikum)
2012, with Tuerk, Nipkow
Manuel Eberl: Efficient and verified computation of Simulation relations on NFAs (Bachelor Thesis)

In Münster

With Markus Müller-Olm

Rene Meis: A Separation Logic Framework for Imperative/HOL (Diploma Thesis)
Rene Meis, Benedikt Nordhoff, Finn Nielson, Stefan Körner: Erweiterung des Isabelle Collection Frameworks (Projektseminar)
Martin Mohr: Ein Datalog-Dialekt mit BDD-Semantik zur symbolischen Analyse paralleler Programme (Diploma Thesis)
Dominik Ulrich: Formalisierung der semantischen Korrektheit der Elimination von totem Code in Isabelle (Bachelor Thesis)

Tutorials for graduates

VTSA 2018: Lecture on Refinement based Algorithm Development with Isabelle/HOL

RS3 Workshop: Tutorial on the Isabelle Refinement Framework and Autoref