| 2026 | ITP | Fractional Separation Logic in Isabelle LLVM. | Peter Lammich |
| 2025 | CAV | A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs. | Bram Kohlen, Maximilian Schffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich |
| 2025 | ITP | Verifying an Efficient Algorithm for Computing Bernoulli Numbers. | Manuel Eberl, Peter Lammich |
| 2024 | FM | Efficient Formally Verified Maximal End Component Decomposition for MDPs. | Arnd Hartmanns, Bram Kohlen, Peter Lammich |
| 2024 | IJCAR | Fast and Verified UNSAT Certificate Checking. | Peter Lammich |
| 2023 | ATVA | Fast Verified SCCs for Probabilistic Model Checking. | Arnd Hartmanns, Bram Kohlen, Peter Lammich |
| 2023 | CADE | A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). | Mathias Fleury, Peter Lammich |
| 2022 | ITP | Refinement of Parallel Algorithms down to LLVM. | Peter Lammich |
| 2021 | ESOP | For a Few Dollars More - Verified Fine-Grained Algorithm Analysis Down to LLVM. | Maximilian P. L. Haslbeck, Peter Lammich |
| 2021 | ITP | Bounded-Deducibility Security (Invited Paper). | Andrei Popescu, Thomas Bauereiss, Peter Lammich |
| 2020 | CADE | Efficient Verified Implementation of Introsort and Pdqsort. | Peter Lammich |
| 2019 | ITP | Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. | Maximilian P. L. Haslbeck, Peter Lammich |
| 2019 | ITP | Generating Verified LLVM from Isabelle/HOL. | Peter Lammich |
| 2019 | ITP | Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. | Peter Lammich, Tobias Nipkow |
| 2019 | SAFECOMP | Formal Verification of Memory Preservation of x86-64 Binaries. | Joshua A. Bockenek, Freek Verbeek, Peter Lammich, Binoy Ravindran |
| 2018 | CPP | A verified SAT solver with watched literals using imperative HOL. | Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich |
| 2018 | ICTAI | A Formally Verified Validator for Classical Planning Problems and Solutions. | Mohammad Abdulaziz, Peter Lammich |
| 2018 | TACAS | Verified Model Checking of Timed Automata. | Simon Wimmer, Peter Lammich |
| 2017 | CADE | Efficient Verified (UN)SAT Certificate Checking. | Peter Lammich |
| 2017 | SAT | The GRAT Tool Chain - Efficient (UN)SAT Certificate Checking with Formal Correctness Guarantees. | Peter Lammich |
| 2016 | CPP | Refinement based verification of imperative data structures. | Peter Lammich |
| 2016 | ITP | Formalizing the Edmonds-Karp Algorithm. | Peter Lammich, S. Reza Sefidgar |
| 2015 | CPP | A Framework for Verifying Depth-First Search Algorithms. | Peter Lammich, Ren Neumann |
| 2015 | ITP | Refinement to Imperative/HOL. | Peter Lammich |
| 2014 | CAV | A Conference Management System with Verified Document Confidentiality. | Sudeep Kanav, Peter Lammich, Andrei Popescu |
| 2014 | ITP | Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm. | Peter Lammich |
| 2013 | CAV | A Fully Verified Executable LTL Model Checker. | Javier Esparza, Peter Lammich, Ren Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus |
| 2013 | ITP | Automatic Data Refinement. | Peter Lammich |
| 2013 | SAS | Contextual Locking for Dynamic Pushdown Networks. | Peter Lammich, Markus Mller-Olm, Helmut Seidl, Alexander Wenner |
| 2012 | ITP | Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm. | Peter Lammich, Thomas Tuerk |
| 2011 | POPL | Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. | Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Peter Lammich, Markus Mller-Olm |
| 2011 | VMCAI | Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation. | Thomas Martin Gawlitza, Peter Lammich, Markus Mller-Olm, Helmut Seidl, Alexander Wenner |
| 2010 | ITP | The Isabelle Collections Framework. | Peter Lammich, Andreas Lochbihler |
| 2009 | CAV | Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints. | Peter Lammich, Markus Mller-Olm, Alexander Wenner |
| 2008 | SAS | Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors. | Peter Lammich, Markus Mller-Olm |
| 2007 | CONCUR | Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures. | Peter Lammich, Markus Mller-Olm |