Peter Lammich
Peter Lammich
The University of Manchester
Verified email at in.tum.de
Title
Cited by
Cited by
Year
A fully verified executable LTL model checker
J Esparza, P Lammich, R Neumann, T Nipkow, A Schimpf, JG Smaus
International Conference on Computer Aided Verification, 463-478, 2013
892013
Automatic data refinement
P Lammich
International Conference on Interactive Theorem Proving, 84-99, 2013
672013
The Isabelle collections framework
P Lammich, A Lochbihler
International Conference on Interactive Theorem Proving, 339-354, 2010
592010
A conference management system with verified document confidentiality
S Kanav, P Lammich, A Popescu
International Conference on Computer Aided Verification, 167-183, 2014
522014
Applying data refinement for monadic programs to Hopcroft’s algorithm
P Lammich, T Tuerk
International Conference on Interactive Theorem Proving, 166-182, 2012
512012
Refinement to imperative/HOL
P Lammich
International Conference on Interactive Theorem Proving, 253-269, 2015
482015
A verified SAT solver framework with learn, forget, restart, and incrementality
JC Blanchette, M Fleury, P Lammich, C Weidenbach
Journal of automated reasoning 61 (1-4), 333-365, 2018
432018
Predecessor sets of dynamic pushdown networks with tree-regular constraints
P Lammich, M Müller-Olm, A Wenner
International Conference on Computer Aided Verification, 525-539, 2009
422009
Efficient verified (UN) SAT certificate checking
P Lammich
International Conference on Automated Deduction, 237-254, 2017
392017
Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation
TM Gawlitza, P Lammich, M Müller-Olm, H Seidl, A Wenner
International Workshop on Verification, Model Checking, and Abstract …, 2011
332011
Refinement based verification of imperative data structures
P Lammich
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016
272016
Verified efficient implementation of Gabow’s strongly connected component algorithm
P Lammich
International Conference on Interactive Theorem Proving, 325-340, 2014
252014
Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol
MD Schwarz, H Seidl, V Vojdani, P Lammich, M Müller-Olm
ACM SIGPLAN Notices 46 (1), 93-104, 2011
242011
Conflict analysis of programs with procedures, dynamic thread creation, and monitors
P Lammich, M Müller-Olm
International Static Analysis Symposium, 205-220, 2008
222008
A framework for verifying depth-first search algorithms
P Lammich, R Neumann
Proceedings of the 2015 Conference on Certified Programs and Proofs, 137-146, 2015
192015
Precise fixpoint-based analysis of programs with thread-creation and procedures
P Lammich, M Müller-Olm
International Conference on Concurrency Theory, 287-302, 2007
192007
Verified model checking of timed automata
S Wimmer, P Lammich
International Conference on Tools and Algorithms for the Construction and …, 2018
182018
Formal verification of an executable LTL model checker with partial order reduction
J Brunner, P Lammich
Journal of Automated Reasoning 60 (1), 3-21, 2018
182018
A verified SAT solver with watched literals using Imperative HOL
M Fleury, JC Blanchette, P Lammich
Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018
172018
Formalizing the edmonds-karp algorithm
P Lammich, SR Sefidgar
International Conference on Interactive Theorem Proving, 219-234, 2016
172016
The system can't perform the operation now. Try again later.
Articles 1–20