Peter Lammich

According to our database, Peter Lammich authored at least 74 papers between 2007 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting.

Peter Lammich

J. Autom. Reason., September, 2024

Difference Bound Matrices.

Simon Wimmer, Peter Lammich

Arch. Formal Proofs, 2024

Worklist Algorithms.

Simon Wimmer, Peter Lammich

Arch. Formal Proofs, 2024

Parallel Shear Sort.

Manuel Eberl, Peter Lammich

Arch. Formal Proofs, 2024

Fast and Verified UNSAT Certificate Checking.

Peter Lammich

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

Efficient Formally Verified Maximal End Component Decomposition for MDPs.

Arnd Hartmanns, Bram Kohlen, Peter Lammich

Proceedings of the Formal Methods - 26th International Symposium, 2024

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

A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper).

Mathias Fleury, Peter Lammich

Proceedings of the Automated Deduction - CADE 29, 2023

Fast Verified SCCs for Probabilistic Model Checking.

Arnd Hartmanns, Bram Kohlen, Peter Lammich

Proceedings of the Automated Technology for Verification and Analysis, 2023

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

Refinement of Parallel Algorithms down to LLVM.

Peter Lammich

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021

CoCon: A Conference Management System with Formally Verified Document Confidentiality.

Andrei Popescu, Peter Lammich, Ping Hou

J. Autom. Reason., 2021

CoCon: A Confidentiality-Verified Conference Management System.

Andrei Popescu, Peter Lammich, Thomas Bauereiss

Arch. Formal Proofs, 2021

van Emde Boas Trees.

Thomas Ammer, Peter Lammich

Arch. Formal Proofs, 2021

Bounded-Deducibility Security (Invited Paper).

Andrei Popescu, Thomas Bauereiss, Peter Lammich

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2020

Efficient Verified (UN)SAT Certificate Checking.

Peter Lammich

J. Autom. Reason., 2020

AI Planning Languages Semantics.

Mohammad Abdulaziz, Peter Lammich

Arch. Formal Proofs, 2020

Efficient Verified Implementation of Introsort and Pdqsort.

Peter Lammich

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL.

Peter Lammich, S. Reza Sefidgar

J. Autom. Reason., 2019

Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches.

Peter Lammich, Andreas Lochbihler

J. Autom. Reason., 2019

Refinement to Imperative HOL.

Peter Lammich

J. Autom. Reason., 2019

VerifyThis 2019 - Polished Isabelle Solutions.

Peter Lammich, Simon Wimmer

Arch. Formal Proofs, 2019

IMP2 - Simple Program Verification in Isabelle/HOL.

Peter Lammich, Simon Wimmer

Arch. Formal Proofs, 2019

Priority Search Trees.

Peter Lammich, Tobias Nipkow

Arch. Formal Proofs, 2019

Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra.

Peter Lammich, Tobias Nipkow

Arch. Formal Proofs, 2019

Kruskal's Algorithm for Minimum Spanning Forest.

Maximilian P. L. Haslbeck, Peter Lammich, Julian Biendarra

Arch. Formal Proofs, 2019

Formal Verification of Memory Preservation of x86-64 Binaries.

Joshua A. Bockenek, Freek Verbeek, Peter Lammich, Binoy Ravindran

Proceedings of the Computer Safety, Reliability, and Security, 2019

Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra.

Peter Lammich, Tobias Nipkow

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Generating Verified LLVM from Isabelle/HOL.

Peter Lammich

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL.

Maximilian P. L. Haslbeck, Peter Lammich

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018

Formal Verification of an Executable LTL Model Checker with Partial Order Reduction.

Julian Brunner, Peter Lammich

J. Autom. Reason., 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

VerifyThis 2018 - Polished Isabelle Solutions.

Peter Lammich, Simon Wimmer

Arch. Formal Proofs, 2018

Verified Model Checking of Timed Automata.

Simon Wimmer, Peter Lammich

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

A Formally Verified Validator for Classical Planning Problems and Solutions.

Mohammad Abdulaziz, Peter Lammich

Proceedings of the IEEE 30th International Conference on Tools with Artificial Intelligence, 2018

A verified SAT solver with watched literals using imperative HOL.

Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

The Floyd-Warshall Algorithm for Shortest Paths.

Simon Wimmer, Peter Lammich

Arch. Formal Proofs, 2017

Formalizing Push-Relabel Algorithms.

Peter Lammich, S. Reza Sefidgar

Arch. Formal Proofs, 2017

Flow Networks and the Min-Cut-Max-Flow Theorem.

Peter Lammich, S. Reza Sefidgar

Arch. Formal Proofs, 2017

The string search algorithm by Knuth, Morris and Pratt.

Fabian Hellauer, Peter Lammich

Arch. Formal Proofs, 2017

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

Peter Lammich

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

2016

Algorithms for Reduced Ordered Binary Decision Diagrams.

Julius Michaelis, Max W. Haslbeck, Peter Lammich, Lars Hupel

Arch. Formal Proofs, 2016

Formalizing the Edmonds-Karp Algorithm.

Peter Lammich, S. Reza Sefidgar

Arch. Formal Proofs, 2016

A Framework for Verifying Depth-First Search Algorithms.

Peter Lammich, René Neumann

Arch. Formal Proofs, 2016

The Imperative Refinement Framework.

Peter Lammich

Arch. Formal Proofs, 2016

Refinement based verification of imperative data structures.

Peter Lammich

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2014

Converting Linear-Time Temporal Logic to Generalized Büchi Automata.

Alexander Schimpf, Peter Lammich

Arch. Formal Proofs, 2014

A shallow embedding of HyperCTL.

Markus N. Rabe, Peter Lammich, Andrei Popescu

Arch. Formal Proofs, 2014

Bounded-Deducibility Security.

Andrei Popescu, Peter Lammich

Arch. Formal Proofs, 2014

The CAVA Automata Library.

Peter Lammich

Arch. Formal Proofs, 2014

Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm.

Peter Lammich

Arch. Formal Proofs, 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 Component Algorithm.

Peter Lammich

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

A Conference Management System with Verified Document Confidentiality.

Sudeep Kanav, Peter Lammich, Andrei Popescu

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Iterable Forward Reachability Analysis of Monitor-DPNs.

Benedikt Nordhoff, Markus Müller-Olm, Peter Lammich

Proceedings of the Semantics, 2013

Automatic Data Refinement.

Peter Lammich

Arch. Formal Proofs, 2013

Contextual Locking for Dynamic Pushdown Networks.

Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner

Proceedings of the Static Analysis - 20th International Symposium, 2013

2012

Dijkstra's Shortest Path Algorithm.

Benedikt Nordhoff, Peter Lammich

Arch. Formal Proofs, 2012

A Separation Logic Framework for Imperative HOL.

Peter Lammich, Rene Meis

Arch. Formal Proofs, 2012

Refinement for Monadic Programs.

Peter Lammich

Arch. Formal Proofs, 2012

Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm.

Peter Lammich, Thomas Tuerk

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

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

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

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 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

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Lock sensitive analysis of parallel programs.

Peter Lammich

PhD thesis, 2011

2010

Finger Trees.

Benedikt Nordhoff, Stefan Körner, Peter Lammich

Arch. Formal Proofs, 2010

Binomial Heaps and Skew Binomial Heaps.

Rene Meis, Finn Nielsen, Peter Lammich

Arch. Formal Proofs, 2010

The Isabelle Collections Framework.

Peter Lammich, Andreas Lochbihler

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

Tree Automata.

Peter Lammich

Arch. Formal Proofs, 2009

Collections Framework.

Peter Lammich

Arch. Formal Proofs, 2009

Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints.

Peter Lammich, Markus Müller-Olm, Alexander Wenner

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors.

Peter Lammich, Markus Müller-Olm

Proceedings of the Static Analysis, 15th International Symposium, 2008

2007

Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors.

Peter Lammich, Markus Müller-Olm

Arch. Formal Proofs, 2007

Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures.

Peter Lammich, Markus Müller-Olm

Proceedings of the CONCUR 2007 - Concurrency Theory, 18th International Conference, 2007