Peter Lammich

Affiliations:
  • University of Münster, Germany


According to our database1, Peter Lammich authored at least 68 papers between 2007 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly.
Proc. ACM Program. Lang., 2023

A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper).
Proceedings of the Automated Deduction - CADE 29, 2023

Fast Verified SCCs for Probabilistic Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2023

2022
For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM.
ACM Trans. Program. Lang. Syst., 2022

Refinement of Parallel Algorithms down to LLVM.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021
CoCon: A Conference Management System with Formally Verified Document Confidentiality.
J. Autom. Reason., 2021

CoCon: A Confidentiality-Verified Conference Management System.
Arch. Formal Proofs, 2021

van Emde Boas Trees.
Arch. Formal Proofs, 2021

Bounded-Deducibility Security (Invited Paper).
Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

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

AI Planning Languages Semantics.
Arch. Formal Proofs, 2020

Efficient Verified Implementation of Introsort and Pdqsort.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019
Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL.
J. Autom. Reason., 2019

Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches.
J. Autom. Reason., 2019

Refinement to Imperative HOL.
J. Autom. Reason., 2019

VerifyThis 2019 - Polished Isabelle Solutions.
Arch. Formal Proofs, 2019

IMP2 - Simple Program Verification in Isabelle/HOL.
Arch. Formal Proofs, 2019

Priority Search Trees.
Arch. Formal Proofs, 2019

Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra.
Arch. Formal Proofs, 2019

Kruskal's Algorithm for Minimum Spanning Forest.
Arch. Formal Proofs, 2019

Formal Verification of Memory Preservation of x86-64 Binaries.
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.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Generating Verified LLVM from Isabelle/HOL.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction.
J. Autom. Reason., 2018

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
J. Autom. Reason., 2018

VerifyThis 2018 - Polished Isabelle Solutions.
Arch. Formal Proofs, 2018

Verified Model Checking of Timed Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

A Formally Verified Validator for Classical Planning Problems and Solutions.
Proceedings of the IEEE 30th International Conference on Tools with Artificial Intelligence, 2018

A verified SAT solver with watched literals using imperative HOL.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017
The Floyd-Warshall Algorithm for Shortest Paths.
Arch. Formal Proofs, 2017

Formalizing Push-Relabel Algorithms.
Arch. Formal Proofs, 2017

Flow Networks and the Min-Cut-Max-Flow Theorem.
Arch. Formal Proofs, 2017

The string search algorithm by Knuth, Morris and Pratt.
Arch. Formal Proofs, 2017

The GRAT Tool Chain - Efficient (UN)SAT Certificate Checking with Formal Correctness Guarantees.
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.
Arch. Formal Proofs, 2016

Formalizing the Edmonds-Karp Algorithm.
Arch. Formal Proofs, 2016

A Framework for Verifying Depth-First Search Algorithms.
Arch. Formal Proofs, 2016

The Imperative Refinement Framework.
Arch. Formal Proofs, 2016

Refinement based verification of imperative data structures.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2014
Converting Linear-Time Temporal Logic to Generalized Büchi Automata.
Arch. Formal Proofs, 2014

A shallow embedding of HyperCTL.
Arch. Formal Proofs, 2014

Bounded-Deducibility Security.
Arch. Formal Proofs, 2014

The CAVA Automata Library.
Arch. Formal Proofs, 2014

Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm.
Arch. Formal Proofs, 2014

A Fully Verified Executable LTL Model Checker.
Arch. Formal Proofs, 2014

Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

A Conference Management System with Verified Document Confidentiality.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
Iterable Forward Reachability Analysis of Monitor-DPNs.
Proceedings of the Semantics, 2013

Automatic Data Refinement.
Arch. Formal Proofs, 2013

Contextual Locking for Dynamic Pushdown Networks.
Proceedings of the Static Analysis - 20th International Symposium, 2013

2012
Dijkstra's Shortest Path Algorithm.
Arch. Formal Proofs, 2012

A Separation Logic Framework for Imperative HOL.
Arch. Formal Proofs, 2012

Refinement for Monadic Programs.
Arch. Formal Proofs, 2012

Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011
A decision procedure for detecting atomicity violations for communicating processes with locks.
Int. J. Softw. Tools Technol. Transf., 2011

Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol.
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Lock sensitive analysis of parallel programs.
PhD thesis, 2011

2010
Finger Trees.
Arch. Formal Proofs, 2010

Binomial Heaps and Skew Binomial Heaps.
Arch. Formal Proofs, 2010

The Isabelle Collections Framework.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009
Tree Automata.
Arch. Formal Proofs, 2009

Collections Framework.
Arch. Formal Proofs, 2009

Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors.
Proceedings of the Static Analysis, 15th International Symposium, 2008

2007
Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors.
Arch. Formal Proofs, 2007

Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures.
Proceedings of the CONCUR 2007 - Concurrency Theory, 18th International Conference, 2007


  Loading...