General

Office Hours: TBA
Homepage at TU Munich

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 up

Initial 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