Peter Lammich

 

Website: http://www21.in.tum.de/~lammich

 

Entries

2019

October 16: VerifyThis 2019 -- Polished Isabelle Solutions

June 25: Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra

June 25: Priority Search Trees

February 14: Kruskal's Algorithm for Minimum Spanning Forest

January 15: IMP2 – Simple Program Verification in Isabelle/HOL

 

2018

April 27: VerifyThis 2018 - Polished Isabelle Solutions

 

2017

December 18: The string search algorithm by Knuth, Morris and Pratt

June 1: Formalizing Push-Relabel Algorithms

June 1: Flow Networks and the Min-Cut-Max-Flow Theorem

May 8: The Floyd-Warshall Algorithm for Shortest Paths

 

2016

August 12: Formalizing the Edmonds-Karp Algorithm

August 8: The Imperative Refinement Framework

July 5: A Framework for Verifying Depth-First Search Algorithms

April 27: Algorithms for Reduced Ordered Binary Decision Diagrams

 

2014

May 28: Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm

May 28: The CAVA Automata Library

May 28: Converting Linear-Time Temporal Logic to Generalized Büchi Automata

May 28: A Fully Verified Executable LTL Model Checker

April 22: Bounded-Deducibility Security

April 16: A shallow embedding of HyperCTL*

 

2013

October 2: Automatic Data Refinement

 

2012

November 14: A Separation Logic Framework for Imperative HOL

January 30: Refinement for Monadic Programs

January 30: Dijkstra's Shortest Path Algorithm

 

2010

October 28: Finger Trees

October 28: Binomial Heaps and Skew Binomial Heaps

 

2009

November 25: Tree Automata

November 25: Collections Framework

 

2007

December 14: Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors