Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures. - Peter Lammich; Markus Müller-Olm (CONCUR, 2007)

Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors. - Peter Lammich; Markus Müller-Olm (Arch. Formal Proofs, 2007)

Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors. - Peter Lammich; Markus Müller-Olm (SAS, 2008)

Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints. - Peter Lammich; Markus Müller-Olm; Alexander Wenner (CAV, 2009)

Collections Framework. - Peter Lammich (Arch. Formal Proofs, 2009)

Tree Automata. - Peter Lammich (Arch. Formal Proofs, 2009)

The Isabelle Collections Framework. - Peter Lammich; Andreas Lochbihler (ITP, 2010)

Binomial Heaps and Skew Binomial Heaps. - Rene Meis; Finn Nielsen; Peter Lammich (Arch. Formal Proofs, 2010)

Finger Trees. - Benedikt Nordhoff; Stefan Körner; Peter Lammich (Arch. Formal Proofs, 2010)

Lock sensitive analysis of parallel programs. - Peter Lammich (2011)

Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. - Martin D. Schwarz; Helmut Seidl; Vesal Vojdani; Peter Lammich; Markus Müller-Olm (POPL, 2011)

Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation. - Thomas Martin Gawlitza; Peter Lammich; Markus Müller-Olm; Helmut Seidl; Alexander Wenner (VMCAI, 2011)

A decision procedure for detecting atomicity violations for communicating processes with locks. - Nicholas Kidd; Peter Lammich; Tayssir Touili; Thomas W. Reps (Int. J. Softw. Tools Technol. Transf., 2011)

Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm. - Peter Lammich; Thomas Tuerk (ITP, 2012)

Refinement for Monadic Programs. - Peter Lammich (Arch. Formal Proofs, 2012)

A Separation Logic Framework for Imperative HOL. - Peter Lammich; Rene Meis (Arch. Formal Proofs, 2012)

Dijkstra's Shortest Path Algorithm. - Benedikt Nordhoff; Peter Lammich (Arch. Formal Proofs, 2012)

Contextual Locking for Dynamic Pushdown Networks. - Peter Lammich; Markus Müller-Olm; Helmut Seidl; Alexander Wenner (SAS, 2013)

Automatic Data Refinement. - Peter Lammich (Arch. Formal Proofs, 2013)

Iterable Forward Reachability Analysis of Monitor-DPNs. - Benedikt Nordhoff; Markus Müller-Olm; Peter Lammich (Festschrift for Dave Schmidt, 2013)

A Conference Management System with Verified Document Confidentiality. - Sudeep Kanav; Peter Lammich; Andrei Popescu 001 (CAV, 2014)

Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm. - Peter Lammich (ITP, 2014)

A Fully Verified Executable LTL Model Checker. - Javier Esparza; Peter Lammich; René Neumann; Tobias Nipkow; Alexander Schimpf; Jan-Georg Smaus (Arch. Formal Proofs, 2014)

Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm. - Peter Lammich (Arch. Formal Proofs, 2014)

The CAVA Automata Library. - Peter Lammich (Arch. Formal Proofs, 2014)

Bounded-Deducibility Security. - Andrei Popescu 001; Peter Lammich (Arch. Formal Proofs, 2014)

A shallow embedding of HyperCTL. - Markus N. Rabe; Peter Lammich; Andrei Popescu 001 (Arch. Formal Proofs, 2014)

Converting Linear-Time Temporal Logic to Generalized Büchi Automata. - Alexander Schimpf; Peter Lammich (Arch. Formal Proofs, 2014)

Refinement based verification of imperative data structures. - Peter Lammich (CPP, 2016)

The Imperative Refinement Framework. - Peter Lammich (Arch. Formal Proofs, 2016)

A Framework for Verifying Depth-First Search Algorithms. - Peter Lammich; René Neumann (Arch. Formal Proofs, 2016)

Formalizing the Edmonds-Karp Algorithm. - Peter Lammich; S. Reza Sefidgar (Arch. Formal Proofs, 2016)

Algorithms for Reduced Ordered Binary Decision Diagrams. - Julius Michaelis; Max W. Haslbeck; Peter Lammich; Lars Hupel (Arch. Formal Proofs, 2016)

The GRAT Tool Chain - Efficient (UN)SAT Certificate Checking with Formal Correctness Guarantees. - Peter Lammich (SAT, 2017)

The string search algorithm by Knuth, Morris and Pratt. - Fabian Hellauer; Peter Lammich (Arch. Formal Proofs, 2017)

Flow Networks and the Min-Cut-Max-Flow Theorem. - Peter Lammich; S. Reza Sefidgar (Arch. Formal Proofs, 2017)

Formalizing Push-Relabel Algorithms. - Peter Lammich; S. Reza Sefidgar (Arch. Formal Proofs, 2017)

The Floyd-Warshall Algorithm for Shortest Paths. - Simon Wimmer 001; Peter Lammich (Arch. Formal Proofs, 2017)

A verified SAT solver with watched literals using imperative HOL. - Mathias Fleury; Jasmin Christian Blanchette; Peter Lammich (CPP, 2018)

A Formally Verified Validator for Classical Planning Problems and Solutions. - Mohammad Abdulaziz; Peter Lammich (ICTAI, 2018)

Verified Model Checking of Timed Automata. - Simon Wimmer 001; Peter Lammich (TACAS (1), 2018)

VerifyThis 2018 - Polished Isabelle Solutions. - Peter Lammich; Simon Wimmer 001 (Arch. Formal Proofs, 2018)

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. - Jasmin Christian Blanchette; Mathias Fleury; Peter Lammich; Christoph Weidenbach (J. Autom. Reason., 2018)

Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. - Julian Brunner 001; Peter Lammich (J. Autom. Reason., 2018)

Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. - Maximilian P. L. Haslbeck; Peter Lammich (ITP, 2019)

Generating Verified LLVM from Isabelle/HOL. - Peter Lammich (ITP, 2019)

Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. - Peter Lammich; Tobias Nipkow (ITP, 2019)

Formal Verification of Memory Preservation of x86-64 Binaries. - Joshua A. Bockenek; Freek Verbeek; Peter Lammich; Binoy Ravindran (SAFECOMP, 2019)

Kruskal's Algorithm for Minimum Spanning Forest. - Maximilian P. L. Haslbeck; Peter Lammich; Julian Biendarra (Arch. Formal Proofs, 2019)

Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra. - Peter Lammich; Tobias Nipkow (Arch. Formal Proofs, 2019)

Priority Search Trees. - Peter Lammich; Tobias Nipkow (Arch. Formal Proofs, 2019)

IMP2 - Simple Program Verification in Isabelle/HOL. - Peter Lammich; Simon Wimmer 001 (Arch. Formal Proofs, 2019)

VerifyThis 2019 - Polished Isabelle Solutions. - Peter Lammich; Simon Wimmer 001 (Arch. Formal Proofs, 2019)

Refinement to Imperative HOL. - Peter Lammich (J. Autom. Reason., 2019)

Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches. - Peter Lammich; Andreas Lochbihler (J. Autom. Reason., 2019)

Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. - Peter Lammich; S. Reza Sefidgar (J. Autom. Reason., 2019)

Efficient Verified Implementation of Introsort and Pdqsort. - Peter Lammich (IJCAR (2), 2020)

AI Planning Languages Semantics. - Mohammad Abdulaziz; Peter Lammich (Arch. Formal Proofs, 2020)

Efficient Verified (UN)SAT Certificate Checking. - Peter Lammich (J. Autom. Reason., 2020)

Bounded-Deducibility Security (Invited Paper). - Andrei Popescu 001; Thomas Bauereiss; Peter Lammich (ITP, 2021)

van Emde Boas Trees. - Thomas Ammer; Peter Lammich (Arch. Formal Proofs, 2021)

CoCon: A Confidentiality-Verified Conference Management System. - Andrei Popescu 001; Peter Lammich; Thomas Bauereiss (Arch. Formal Proofs, 2021)

CoCon: A Conference Management System with Formally Verified Document Confidentiality. - Andrei Popescu 001; Peter Lammich; Ping Hou (J. Autom. Reason., 2021)

Refinement of Parallel Algorithms down to LLVM. - Peter Lammich (ITP, 2022)

For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM. - Maximilian P. L. Haslbeck; Peter Lammich (ACM Trans. Program. Lang. Syst., 2022)

Fast Verified SCCs for Probabilistic Model Checking. - Arnd Hartmanns; Bram Kohlen; Peter Lammich (ATVA (1), 2023)

A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). - Mathias Fleury; Peter Lammich (CADE, 2023)

WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly. - Conrad Watt; Maja Trela; Peter Lammich; Florian Märkl (Proc. ACM Program. Lang., 2023)

Efficient Formally Verified Maximal End Component Decomposition for MDPs. - Arnd Hartmanns; Bram Kohlen; Peter Lammich (FM (1), 2024)

Fast and Verified UNSAT Certificate Checking. - Peter Lammich (IJCAR (1), 2024)

Parallel Shear Sort. - Manuel Eberl; Peter Lammich (Arch. Formal Proofs, 2024)

Worklist Algorithms. - Simon Wimmer 001; Peter Lammich (Arch. Formal Proofs, 2024)

Difference Bound Matrices. - Simon Wimmer 001; Peter Lammich (Arch. Formal Proofs, 2024)

Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting. - Peter Lammich (J. Autom. Reason., 2024)

A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs. - Bram Kohlen; Maximilian Schäffeler; Mohammad Abdulaziz; Arnd Hartmanns; Peter Lammich (CAV (2), 2025)