
Short Summary
I'm a research assistant professor at the Systems Software Research Group at Virginia Tech. 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.News
Homepage at VT set upInitial setup of my VT homepage
Selected Publications
-
Peter Lammich
Efficient Verified (UN)SAT Certificate Checking
Proc. of CADE 2017
pub/cade2017.pdf
-
Peter Lammich.
Refinement to Imperative/HOL
In Proc. of ITP 2015 (Interactive Theorem Proving), Springer 2015.
pub/itp15_sepref.pdf
-
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 -
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