# Peter Lammich

According to our database

Collaborative distances:

^{1}, Peter Lammich authored at least 49 papers between 2007 and 2019.Collaborative distances:

## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### Homepage:

#### On csauthors.net:

## Bibliography

2019

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

J. Autom. Reasoning, 2019

IMP2 - Simple Program Verification in Isabelle/HOL.

Archive of Formal Proofs, 2019

Kruskal's Algorithm for Minimum Spanning Forest.

Archive of Formal Proofs, 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 Floyd-Warshall Algorithm for Shortest Paths.

Archive of Formal Proofs, 2017

Formalizing Push-Relabel Algorithms.

Archive of Formal Proofs, 2017

Flow Networks and the Min-Cut-Max-Flow 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 Edmonds-Karp 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 Depth-First Search Algorithms.

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014

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

Archive of Formal Proofs, 2014

A shallow embedding of HyperCTL.

Archive of Formal Proofs, 2014

Bounded-Deducibility 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 Monitor-DPNs.

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

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.

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 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.

Archive of 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