Peter Lammich - RankMe

87 papers A* 4A 4B 21Journal 48Unranked 9

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs. CAV (2) Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich
2025	J	`jnl`	A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs. CoRR Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich
2025	J	`jnl`	Dynamic Pushdown Networks. Arch. Formal Proofs Peter Lammich
2025	B	`conf`	Verifying an Efficient Algorithm for Computing Bernoulli Numbers. ITP Manuel Eberl, Peter Lammich
2024	J	`jnl`	Difference Bound Matrices. Arch. Formal Proofs Simon Wimmer, Peter Lammich
2024	—	`conf`	Efficient Formally Verified Maximal End Component Decomposition for MDPs. FM (1) Arnd Hartmanns, Bram Kohlen, Peter Lammich
2024	—	`conf`	Fast and Verified UNSAT Certificate Checking. IJCAR (1) Peter Lammich
2024	J	`jnl`	Parallel Shear Sort. Arch. Formal Proofs Manuel Eberl, Peter Lammich
2024	J	`jnl`	Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting. J. Autom. Reason. Peter Lammich
2024	J	`jnl`	Worklist Algorithms. Arch. Formal Proofs Simon Wimmer, Peter Lammich
2023	A	`conf`	A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). CADE Mathias Fleury, Peter Lammich
2023	—	`conf`	Fast Verified SCCs for Probabilistic Model Checking. ATVA (1) Arnd Hartmanns, Bram Kohlen, Peter Lammich
2023	J	`jnl`	WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly. Proc. ACM Program. Lang. Conrad Watt, Maja Trela, Peter Lammich, Florian Märkl
2022	J	`jnl`	For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM. ACM Trans. Program. Lang. Syst. Maximilian P. L. Haslbeck, Peter Lammich
2022	B	`conf`	Refinement of Parallel Algorithms down to LLVM. ITP Peter Lammich
2021	B	`conf`	Bounded-Deducibility Security (Invited Paper). ITP Andrei Popescu, Thomas Bauereiss, Peter Lammich
2021	J	`jnl`	CoCon: A Conference Management System with Formally Verified Document Confidentiality. J. Autom. Reason. Andrei Popescu, Peter Lammich, Ping Hou
2021	J	`jnl`	CoCon: A Confidentiality-Verified Conference Management System. Arch. Formal Proofs Andrei Popescu, Peter Lammich, Thomas Bauereiss
2021	A	`conf`	For a Few Dollars More - Verified Fine-Grained Algorithm Analysis Down to LLVM. ESOP Maximilian P. L. Haslbeck, Peter Lammich
2021	J	`jnl`	van Emde Boas Trees. Arch. Formal Proofs Thomas Ammer, Peter Lammich
2020	J	`jnl`	AI Planning Languages Semantics. Arch. Formal Proofs Mohammad Abdulaziz, Peter Lammich
2020	J	`jnl`	Efficient Verified (UN)SAT Certificate Checking. J. Autom. Reason. Peter Lammich
2020	—	`conf`	Efficient Verified Implementation of Introsort and Pdqsort. IJCAR (2) Peter Lammich
2019	J	`jnl`	Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches. J. Autom. Reason. Peter Lammich, Andreas Lochbihler
2019	B	`conf`	Formal Verification of Memory Preservation of x86-64 Binaries. SAFECOMP Joshua A. Bockenek, Freek Verbeek, Peter Lammich, Binoy Ravindran
2019	J	`jnl`	Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. J. Autom. Reason. Peter Lammich, S. Reza Sefidgar
2019	B	`conf`	Generating Verified LLVM from Isabelle/HOL. ITP Peter Lammich
2019	J	`jnl`	IMP2 - Simple Program Verification in Isabelle/HOL. Arch. Formal Proofs Peter Lammich, Simon Wimmer
2019	J	`jnl`	Kruskal's Algorithm for Minimum Spanning Forest. Arch. Formal Proofs Maximilian P. L. Haslbeck, Peter Lammich, Julian Biendarra
2019	J	`jnl`	Priority Search Trees. Arch. Formal Proofs Peter Lammich, Tobias Nipkow
2019	B	`conf`	Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. ITP Peter Lammich, Tobias Nipkow
2019	J	`jnl`	Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra. Arch. Formal Proofs Peter Lammich, Tobias Nipkow
2019	J	`jnl`	Refinement to Imperative HOL. J. Autom. Reason. Peter Lammich
2019	B	`conf`	Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. ITP Maximilian P. L. Haslbeck, Peter Lammich
2019	J	`jnl`	VerifyThis 2019 - Polished Isabelle Solutions. Arch. Formal Proofs Peter Lammich, Simon Wimmer
2018	B	`conf`	A Formally Verified Validator for Classical Planning Problems and Solutions. ICTAI Mohammad Abdulaziz, Peter Lammich
2018	J	`jnl`	A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason. Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
2018	B	`conf`	A verified SAT solver with watched literals using imperative HOL. CPP Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich
2018	J	`jnl`	Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. J. Autom. Reason. Julian Brunner, Peter Lammich
2018	—	`conf`	Verified Model Checking of Timed Automata. TACAS (1) Simon Wimmer, Peter Lammich
2018	J	`jnl`	VerifyThis 2018 - Polished Isabelle Solutions. Arch. Formal Proofs Peter Lammich, Simon Wimmer
2017	A	`conf`	Efficient Verified (UN)SAT Certificate Checking. CADE Peter Lammich
2017	J	`jnl`	Flow Networks and the Min-Cut-Max-Flow Theorem. Arch. Formal Proofs Peter Lammich, S. Reza Sefidgar
2017	J	`jnl`	Formalizing Push-Relabel Algorithms. Arch. Formal Proofs Peter Lammich, S. Reza Sefidgar
2017	J	`jnl`	The Floyd-Warshall Algorithm for Shortest Paths. Arch. Formal Proofs Simon Wimmer, Peter Lammich
2017	A	`conf`	The GRAT Tool Chain - Efficient (UN)SAT Certificate Checking with Formal Correctness Guarantees. SAT Peter Lammich
2017	J	`jnl`	The string search algorithm by Knuth, Morris and Pratt. Arch. Formal Proofs Fabian Hellauer, Peter Lammich
2016	J	`jnl`	A Framework for Verifying Depth-First Search Algorithms. Arch. Formal Proofs Peter Lammich, René Neumann
2016	J	`jnl`	Algorithms for Reduced Ordered Binary Decision Diagrams. Arch. Formal Proofs Julius Michaelis, Max W. Haslbeck, Peter Lammich, Lars Hupel
2016	—	`conf`	Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. NFM Julian Brunner, Peter Lammich
2016	B	`conf`	Formalizing the Edmonds-Karp Algorithm. ITP Peter Lammich, S. Reza Sefidgar
2016	J	`jnl`	Formalizing the Edmonds-Karp Algorithm. Arch. Formal Proofs Peter Lammich, S. Reza Sefidgar
2016	B	`conf`	Refinement based verification of imperative data structures. CPP Peter Lammich
2016	J	`jnl`	The Imperative Refinement Framework. Arch. Formal Proofs Peter Lammich
2015	B	`conf`	A Framework for Verifying Depth-First Search Algorithms. CPP Peter Lammich, René Neumann
2015	B	`conf`	Refinement to Imperative/HOL. ITP Peter Lammich
2014	A*	`conf`	A Conference Management System with Verified Document Confidentiality. CAV Sudeep Kanav, Peter Lammich, Andrei Popescu
2014	J	`jnl`	A Fully Verified Executable LTL Model Checker. Arch. Formal Proofs Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
2014	J	`jnl`	A shallow embedding of HyperCTL. Arch. Formal Proofs Markus N. Rabe, Peter Lammich, Andrei Popescu
2014	J	`jnl`	Bounded-Deducibility Security. Arch. Formal Proofs Andrei Popescu, Peter Lammich
2014	J	`jnl`	Converting Linear-Time Temporal Logic to Generalized Büchi Automata. Arch. Formal Proofs Alexander Schimpf, Peter Lammich
2014	J	`jnl`	The CAVA Automata Library. Arch. Formal Proofs Peter Lammich
2014	B	`conf`	Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm. ITP Peter Lammich
2014	J	`jnl`	Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm. Arch. Formal Proofs Peter Lammich
2013	A*	`conf`	A Fully Verified Executable LTL Model Checker. CAV Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
2013	B	`conf`	Automatic Data Refinement. ITP Peter Lammich
2013	J	`jnl`	Automatic Data Refinement. Arch. Formal Proofs Peter Lammich
2013	B	`conf`	Contextual Locking for Dynamic Pushdown Networks. SAS Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner
2013	—	`conf`	Iterable Forward Reachability Analysis of Monitor-DPNs. Festschrift for Dave Schmidt Benedikt Nordhoff, Markus Müller-Olm, Peter Lammich
2012	J	`jnl`	A Separation Logic Framework for Imperative HOL. Arch. Formal Proofs Peter Lammich, Rene Meis
2012	B	`conf`	Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm. ITP Peter Lammich, Thomas Tuerk
2012	J	`jnl`	Dijkstra's Shortest Path Algorithm. Arch. Formal Proofs Benedikt Nordhoff, Peter Lammich
2012	J	`jnl`	Refinement for Monadic Programs. Arch. Formal Proofs Peter Lammich
2011	J	`jnl`	A decision procedure for detecting atomicity violations for communicating processes with locks. Int. J. Softw. Tools Technol. Transf. Nicholas Kidd, Peter Lammich, Tayssir Touili, Thomas W. Reps
2011	B	`conf`	Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation. VMCAI Thomas Martin Gawlitza, Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner
2011	—	`—`	Lock sensitive analysis of parallel programs. Peter Lammich
2011	A*	`conf`	Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. POPL Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Peter Lammich, Markus Müller-Olm
2010	J	`jnl`	Binomial Heaps and Skew Binomial Heaps. Arch. Formal Proofs Rene Meis, Finn Nielsen, Peter Lammich
2010	J	`jnl`	Finger Trees. Arch. Formal Proofs Benedikt Nordhoff, Stefan Körner, Peter Lammich
2010	B	`conf`	The Isabelle Collections Framework. ITP Peter Lammich, Andreas Lochbihler
2009	—	`conf`	A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks. SPIN Nicholas Kidd, Peter Lammich, Tayssir Touili, Thomas W. Reps
2009	J	`jnl`	Collections Framework. Arch. Formal Proofs Peter Lammich
2009	A*	`conf`	Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints. CAV Peter Lammich, Markus Müller-Olm, Alexander Wenner
2009	J	`jnl`	Tree Automata. Arch. Formal Proofs Peter Lammich
2008	B	`conf`	Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors. SAS Peter Lammich, Markus Müller-Olm
2007	J	`jnl`	Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors. Arch. Formal Proofs Peter Lammich, Markus Müller-Olm
2007	B	`conf`	Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures. CONCUR Peter Lammich, Markus Müller-Olm