Peter Lammich

According to our database1, Peter Lammich authored at least 57 papers between 2007 and 2020.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

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

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

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

Refinement to Imperative HOL.
J. Autom. Reasoning, 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. Reasoning, 2018

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
J. Autom. Reasoning, 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...