Peter Lammich

Technische Universität München
Institut für Informatik
Boltzmannstr. 3
85748 Garching
Deutschland
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: My VT-homepage should appear here soon

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.

CV

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

Publications

Journals

Conferences

Theses

Archive of Formal Proofs

Others

Unpublished Isabelle/HOL projects.

Teaching

Lectures

SS15
Lecture: Automata II: Tree Automata
SS15
Proseminar: SAT-Solvers - Theory, Tools and Applications
WS14/15
Program Optimization
WS14/15
Semantics of Programming Languages

Tutorials of Lectures

SS14
Tutorial of Einführung i.d. Theoretische Informatik
WS13/14
Tutorial of Semantics of Programming Languages
SS13
Tutorial of Equational Logic
WS12/13
Tutorial of Semantics of Programming Languages
SS12
Tutorial of Equational Logic
WS11/12
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

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)
2012
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

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

Tutorials for graduates

Tutorial on the Isabelle Refinement Framework and Autoref