GeneralOffice Hours: TBA
Homepage at TU Munich
Short SummaryI'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.
NewsHomepage at VT set up
Initial setup of my VT homepage
Efficient Verified (UN)SAT Certificate Checking
Proc. of CADE 2017
Refinement to Imperative/HOL
In Proc. of ITP 2015 (Interactive Theorem Proving), Springer 2015.
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.
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.