Peter Lammich
According to our database^{1},
Peter Lammich
authored at least 57 papers
between 2007 and 2019.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at orcid.org
On csauthors.net:
Bibliography
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
IMP2  Simple Program Verification in Isabelle/HOL.
Archive of Formal Proofs, 2019
Priority Search Trees.
Archive of Formal Proofs, 2019
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra.
Archive of Formal Proofs, 2019
Kruskal's Algorithm for Minimum Spanning Forest.
Archive of Formal Proofs, 2019
Formal Verification of Memory Preservation of x8664 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 RunTime of Algorithms in Isabelle/HOL.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019
2018
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
J. Autom. Reasoning, 2018
VerifyThis 2018  Polished Isabelle Solutions.
Archive of 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 FloydWarshall Algorithm for Shortest Paths.
Archive of Formal Proofs, 2017
Formalizing PushRelabel Algorithms.
Archive of Formal Proofs, 2017
Flow Networks and the MinCutMaxFlow Theorem.
Archive of Formal Proofs, 2017
The string search algorithm by Knuth, Morris and Pratt.
Archive of 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
Efficient Verified (UN)SAT Certificate Checking.
Proceedings of the Automated Deduction  CADE 26, 2017
2016
Algorithms for Reduced Ordered Binary Decision Diagrams.
Archive of Formal Proofs, 2016
The Imperative Refinement Framework.
Archive of Formal Proofs, 2016
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction.
Proceedings of the NASA Formal Methods  8th International Symposium, 2016
Formalizing the EdmondsKarp Algorithm.
Proceedings of the Interactive Theorem Proving  7th International Conference, 2016
Refinement based verification of imperative data structures.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016
2015
Refinement to Imperative/HOL.
Proceedings of the Interactive Theorem Proving  6th International Conference, 2015
A Framework for Verifying DepthFirst Search Algorithms.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015
2014
Converting LinearTime Temporal Logic to Generalized Büchi Automata.
Archive of Formal Proofs, 2014
A shallow embedding of HyperCTL.
Archive of Formal Proofs, 2014
BoundedDeducibility Security.
Archive of Formal Proofs, 2014
The CAVA Automata Library.
Archive of Formal Proofs, 2014
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm.
Archive of 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 MonitorDPNs.
Proceedings of the Semantics, 2013
Contextual Locking for Dynamic Pushdown Networks.
Proceedings of the Static Analysis  20th International Symposium, 2013
Automatic Data Refinement.
Proceedings of the Interactive Theorem Proving  4th International Conference, 2013
A Fully Verified Executable LTL Model Checker.
Proceedings of the Computer Aided Verification  25th International Conference, 2013
2012
Dijkstra's Shortest Path Algorithm.
Archive of Formal Proofs, 2012
A Separation Logic Framework for Imperative HOL.
Archive of Formal Proofs, 2012
Refinement for Monadic Programs.
Archive of Formal Proofs, 2012
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm.
Proceedings of the Interactive Theorem Proving  Third International Conference, 2012
2011
JoinLockSensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011
Static analysis of interruptdriven programs synchronized via the priority ceiling protocol.
Proceedings of the 38th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2011
Lock sensitive analysis of parallel programs.
PhD thesis, 2011
2010
Finger Trees.
Archive of Formal Proofs, 2010
Binomial Heaps and Skew Binomial Heaps.
Archive of Formal Proofs, 2010
The Isabelle Collections Framework.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010
2009
Tree Automata.
Archive of Formal Proofs, 2009
Collections Framework.
Archive of Formal Proofs, 2009
A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks.
Proceedings of the Model Checking Software, 2009
Predecessor Sets of Dynamic Pushdown Networks with TreeRegular 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.
Archive of Formal Proofs, 2007
Precise FixpointBased Analysis of Programs with ThreadCreation and Procedures.
Proceedings of the CONCUR 2007  Concurrency Theory, 18th International Conference, 2007