|
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: 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.
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
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 339-354. Springer, 2010. itp10.pdf ©Springer
Verified Model-Checkers
-
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 Jan-Georg 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üller-Olm, 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üller-Olm, and Alexander Wenner.
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular 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
Lock-Sensitive Analysis of Parallel Programs.
Dissertation in Informatik an der WWU Münster
diss11.pdf -
Peter Lammich
Fixpunktbasierte, optimale Analyse von Programmen mit Thread-Erzeugung
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 Model-Checking 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 Hedge-Constrained 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, Markus-Müller Olm
Precise Fixed Point Based Analysis of Programs with Thread-Creation.
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: SAT-Solvers - 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ü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)
- 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
VTSA 2018: Lecture on Refinement based Algorithm Development with Isabelle/HOL
RS3 Workshop: Tutorial on the Isabelle Refinement Framework and Autoref