Technische Universität München Institut für Informatik Boltzmannstr. 3 85748 Garching Deutschland  
Telephone:  +49 (89) 28917326 
Telefax:  +49 (89) 28917307 
Office:  MI 00.09.065 
From August 2017 to February 2018, I am research assistant professor at Virginia Tech.
For TUMStudents: You can still contact me by mail!
For VTStudents: Homepage at VT
I am a researcher (postdoc) at the chair for logic and verification of Prof. Tobias Nipkow.
My main research interest is the production of verified software by a topdown 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 webservices 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üllerOlm.
 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
See DBLP for a complete listHighlights
Refinement Framework

Peter Lammich.
Refinement to Imperative/HOL
To appear in Journal of Automated Reasoning pub/jar_ref_imp_hol.pdf

Peter Lammich and Andreas Lochbihler.
Automatic Refinement to Efficient Data Structures  A comparison of two approaches
To appear in Journal of Automated Reasoning pub/jar_ref_imp_hol.pdf

Peter Lammich.
Automatic Data Refinement
In Proc. of ITP 2013 (Interactive Theorem Proving), Springer 2013.
autoref.pdf

Peter Lammich and Andreas Lochbihler.
The Isabelle Collections Framework.
In Proceedings of ITP 2010
LNCS 6172, pages 339354. Springer, 2010. itp10.pdf ©Springer
Verified ModelCheckers

Simon Wimmer and Peter Lammich:
Verified Model Checking of Timed Automata
Proc. of TACAS 2018
pub/tacas2018.pdf

Julian Brunner, Peter Lammich.
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction.
In Journal of Automatic Reasoning, S.I. NFM16, to appear
JAR17_POR.pdf ©Springer

Peter Lammich
Efficient Verified (UN)SAT Certificate Checking
Proc. of CADE 2017
pub/cade2017.pdf

Javier Esparza, Peter Lammich, Rene Neumann, Tobias Nipkow, Alexander Schimpf, and JanGeorg Smaus.
A Fully Verified Executable LTL Model Checker
In Proc. of CAV 2013 (Computer Aided Verification), Springer 2013.
verified_ltl_paper.pdf
AFP Entry
Verified Security

Sudeep Kanav, Peter Lammich, and Andrei Popescu.
A Conference Management System with Verified Document Confidentiality
In Proc. of CAV 2014 (Computer Aided Verification), Springer 2014.
confsys.pdf
Dynamic Pushdown Networks

Peter Lammich, Markus MüllerOlm, Helmut Seidl, and Alexander Wenner.
Contextual Locking for Dynamic Pushdown Networks
To appear in Proc. of SAS 2013 (Static Analysis Symposium), Springer 2013.
sas13.pdf 
Peter Lammich, Markus MüllerOlm, and Alexander Wenner.
Predecessor Sets of Dynamic Pushdown Networks with TreeRegular Constraints.
In proceedings of CAV'09,
cav09.ps.gz or cav09.pdf ©Springer
Most of the results in this paper have been verified with the theorem prover Isabelle/HOL. For details see the technical report.
Theses

Peter Lammich
LockSensitive Analysis of Parallel Programs.
Dissertation in Informatik an der WWU Münster
diss11.pdf 
Peter Lammich
Fixpunktbasierte, optimale Analyse von Programmen mit ThreadErzeugung
2006 (Diplomarbeit am Fachbereich Informatik der Universität Dortmund)
Others
Unpublished Isabelle/HOL projects.

Peter Lammich
The CAVA Automata Library.
Isabelle Workshop 2014
kps11.pdf 
Peter Lammich
Data Refinement for Verified ModelChecking Algorithms in Isabelle/HOL.
Tagungsband des 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS 2011).
kps11.pdf 
Peter Lammich
Tree Automata for Analyzing Dynamic Pushdown Networks.
Tagungsband des 15. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS 2009).
kps09.pdf 
Peter Lammich
Isabelle Formalization of HedgeConstrained pre* and DPNs with Locks.
Technical Report, Univ. of Münster, January 2009.
Contains proofs for most of the results of our CAV'09 paper.
Proof Document Proof Outline (Proofs skipped) Sources

Peter Lammich, MarkusMüller Olm
Precise Fixed Point Based Analysis of Programs with ThreadCreation.
In Proc. of MEMICS 2006, published by Faculty of Information Technology, Brno University of Technology, 2006. [pdf] [ps]
Teaching
Lectures
 Fall17
 Certified Programming (at Virginia Tech)
 SS15
 Lecture: Automata II: Tree Automata
 SS15
 Proseminar: SATSolvers  Theory, Tools and Applications
 WS14/15, WS16/17
 Program Optimization
 WS14/15
 Semantics of Programming Languages
Tutorials of Lectures
To be updated. 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üllerOlm'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 OnTheFly 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üllerOlm
 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 DatalogDialekt mit BDDSemantik 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
VTSA 2018: Lecture on Refinement based Algorithm Development with Isabelle/HOL
RS3 Workshop: Tutorial on the Isabelle Refinement Framework and Autoref