Peter Lammich

ORCID

Publication Activity (10 Years)

Years Active: 2007-2024
Publications (10 Years): 47

Top Venues

University of Münster (PHD)

Education History

University of Münster

PHD

Publications

Peter Lammich
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting. J. Autom. Reason. 68 (3) (2024)
Simon Wimmer, Peter Lammich
Worklist Algorithms. Arch. Formal Proofs 2024 (2024)
Peter Lammich
Fast and Verified UNSAT Certificate Checking. IJCAR (1) (2024)
Arnd Hartmanns, Bram Kohlen, Peter Lammich
Fast Verified SCCs for Probabilistic Model Checking. ATVA (1) (2023)
Mathias Fleury, Peter Lammich
A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). CADE (2023)
Conrad Watt, Maja Trela, Peter Lammich, Florian Märkl
WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Peter Lammich
Refinement of Parallel Algorithms down to LLVM. ITP (2022)
Maximilian P. L. Haslbeck, Peter Lammich
For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM. ACM Trans. Program. Lang. Syst. 44 (3) (2022)
Andrei Popescu, Thomas Bauereiss, Peter Lammich
Bounded-Deducibility Security (Invited Paper). ITP (2021)
Andrei Popescu, Peter Lammich, Ping Hou
CoCon: A Conference Management System with Formally Verified Document Confidentiality. J. Autom. Reason. 65 (2) (2021)
Thomas Ammer, Peter Lammich
van Emde Boas Trees. Arch. Formal Proofs 2021 (2021)
Maximilian P. L. Haslbeck, Peter Lammich
For a Few Dollars More - Verified Fine-Grained Algorithm Analysis Down to LLVM. ESOP (2021)
Andrei Popescu, Peter Lammich, Thomas Bauereiss
CoCon: A Confidentiality-Verified Conference Management System. Arch. Formal Proofs 2021 (2021)
Mohammad Abdulaziz, Peter Lammich
AI Planning Languages Semantics. Arch. Formal Proofs 2020 (2020)
Peter Lammich
Efficient Verified Implementation of Introsort and Pdqsort. IJCAR (2) (2020)
Peter Lammich
Efficient Verified (UN)SAT Certificate Checking. J. Autom. Reason. 64 (3) (2020)
Joshua A. Bockenek, Freek Verbeek, Peter Lammich, Binoy Ravindran
Formal Verification of Memory Preservation of x86-64 Binaries. SAFECOMP (2019)
Peter Lammich
Generating Verified LLVM from Isabelle/HOL. ITP (2019)
Peter Lammich, Simon Wimmer
IMP2 - Simple Program Verification in Isabelle/HOL. Arch. Formal Proofs 2019 (2019)
Peter Lammich, S. Reza Sefidgar
Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. J. Autom. Reason. 62 (2) (2019)
Peter Lammich, Tobias Nipkow
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra. Arch. Formal Proofs 2019 (2019)
Peter Lammich, Andreas Lochbihler
Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches. J. Autom. Reason. 63 (1) (2019)
Peter Lammich, Tobias Nipkow
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. ITP (2019)
Maximilian P. L. Haslbeck, Peter Lammich
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. ITP (2019)
Peter Lammich
Refinement to Imperative HOL. J. Autom. Reason. 62 (4) (2019)
Peter Lammich, Tobias Nipkow
Priority Search Trees. Arch. Formal Proofs 2019 (2019)
Maximilian P. L. Haslbeck, Peter Lammich, Julian Biendarra
Kruskal's Algorithm for Minimum Spanning Forest. Arch. Formal Proofs 2019 (2019)
Peter Lammich, Simon Wimmer
VerifyThis 2019 - Polished Isabelle Solutions. Arch. Formal Proofs 2019 (2019)
Simon Wimmer, Peter Lammich
Verified Model Checking of Timed Automata. TACAS (1) (2018)
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason. 61 (1-4) (2018)
Julian Brunner, Peter Lammich
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. J. Autom. Reason. 60 (1) (2018)
Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich
A verified SAT solver with watched literals using imperative HOL. CPP (2018)
Peter Lammich, Simon Wimmer
VerifyThis 2018 - Polished Isabelle Solutions. Arch. Formal Proofs 2018 (2018)
Mohammad Abdulaziz, Peter Lammich
A Formally Verified Validator for Classical Planning Problems and Solutions. ICTAI (2018)
Peter Lammich, S. Reza Sefidgar
Formalizing Push-Relabel Algorithms. Arch. Formal Proofs 2017 (2017)
Fabian Hellauer, Peter Lammich
The string search algorithm by Knuth, Morris and Pratt. Arch. Formal Proofs 2017 (2017)
Peter Lammich, S. Reza Sefidgar
Flow Networks and the Min-Cut-Max-Flow Theorem. Arch. Formal Proofs 2017 (2017)
Simon Wimmer, Peter Lammich
The Floyd-Warshall Algorithm for Shortest Paths. Arch. Formal Proofs 2017 (2017)
Peter Lammich
Efficient Verified (UN)SAT Certificate Checking. CADE (2017)
Peter Lammich
The GRAT Tool Chain - Efficient (UN)SAT Certificate Checking with Formal Correctness Guarantees. SAT (2017)
Peter Lammich
The Imperative Refinement Framework. Arch. Formal Proofs 2016 (2016)
Peter Lammich, René Neumann
A Framework for Verifying Depth-First Search Algorithms. Arch. Formal Proofs 2016 (2016)
Julian Brunner, Peter Lammich
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. NFM (2016)
Julius Michaelis, Max W. Haslbeck, Peter Lammich, Lars Hupel
Algorithms for Reduced Ordered Binary Decision Diagrams. Arch. Formal Proofs 2016 (2016)
Peter Lammich
Refinement based verification of imperative data structures. CPP (2016)
Peter Lammich, S. Reza Sefidgar
Formalizing the Edmonds-Karp Algorithm. Arch. Formal Proofs 2016 (2016)
Peter Lammich, S. Reza Sefidgar
Formalizing the Edmonds-Karp Algorithm. ITP (2016)
Peter Lammich
Refinement to Imperative/HOL. ITP (2015)
Peter Lammich, René Neumann
A Framework for Verifying Depth-First Search Algorithms. CPP (2015)
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
A Fully Verified Executable LTL Model Checker. Arch. Formal Proofs 2014 (2014)
Andrei Popescu, Peter Lammich
Bounded-Deducibility Security. Arch. Formal Proofs 2014 (2014)
Sudeep Kanav, Peter Lammich, Andrei Popescu
A Conference Management System with Verified Document Confidentiality. CAV (2014)
Peter Lammich
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm. Arch. Formal Proofs 2014 (2014)
Markus N. Rabe, Peter Lammich, Andrei Popescu
A shallow embedding of HyperCTL. Arch. Formal Proofs 2014 (2014)
Alexander Schimpf, Peter Lammich
Converting Linear-Time Temporal Logic to Generalized Büchi Automata. Arch. Formal Proofs 2014 (2014)
Peter Lammich
The CAVA Automata Library. Arch. Formal Proofs 2014 (2014)
Peter Lammich
Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm. ITP (2014)
Benedikt Nordhoff, Markus Müller-Olm, Peter Lammich
Iterable Forward Reachability Analysis of Monitor-DPNs. Festschrift for Dave Schmidt (2013)
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
A Fully Verified Executable LTL Model Checker. CAV (2013)
Peter Lammich
Automatic Data Refinement. Arch. Formal Proofs 2013 (2013)
Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner
Contextual Locking for Dynamic Pushdown Networks. SAS (2013)
Peter Lammich
Automatic Data Refinement. ITP (2013)
Peter Lammich, Thomas Tuerk
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm. ITP (2012)
Peter Lammich
Refinement for Monadic Programs. Arch. Formal Proofs 2012 (2012)
Peter Lammich, Rene Meis
A Separation Logic Framework for Imperative HOL. Arch. Formal Proofs 2012 (2012)
Benedikt Nordhoff, Peter Lammich
Dijkstra's Shortest Path Algorithm. Arch. Formal Proofs 2012 (2012)
Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Peter Lammich, Markus Müller-Olm
Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. POPL (2011)
Thomas Martin Gawlitza, Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner
Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation. VMCAI (2011)
Nicholas Kidd, Peter Lammich, Tayssir Touili, Thomas W. Reps
A decision procedure for detecting atomicity violations for communicating processes with locks. Int. J. Softw. Tools Technol. Transf. 13 (1) (2011)
Benedikt Nordhoff, Stefan Körner, Peter Lammich
Finger Trees. Arch. Formal Proofs 2010 (2010)
Peter Lammich, Andreas Lochbihler
The Isabelle Collections Framework. ITP (2010)
Rene Meis, Finn Nielsen, Peter Lammich
Binomial Heaps and Skew Binomial Heaps. Arch. Formal Proofs 2010 (2010)
Peter Lammich
Collections Framework. Arch. Formal Proofs 2009 (2009)
Peter Lammich
Tree Automata. Arch. Formal Proofs 2009 (2009)
Peter Lammich, Markus Müller-Olm, Alexander Wenner
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints. CAV (2009)
Nicholas Kidd, Peter Lammich, Tayssir Touili, Thomas W. Reps
A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks. SPIN (2009)
Peter Lammich, Markus Müller-Olm
Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors. SAS (2008)
Peter Lammich, Markus Müller-Olm
Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures. CONCUR (2007)
Peter Lammich, Markus Müller-Olm
Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors. Arch. Formal Proofs 2007 (2007)

Peter Lammich

Publication Activity (10 Years)

Top Topics

Top Venues