| A fully verified executable LTL model checker J Esparza, P Lammich, R Neumann, T Nipkow, A Schimpf, JG Smaus Computer Aided Verification: 25th International Conference, CAV 2013, Saint …, 2013 | 121 | 2013 |
| Refinement to imperative HOL P Lammich Journal of Automated Reasoning 62 (4), 481-503, 2019 | 92 | 2019 |
| Automatic data refinement P Lammich Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013 | 84 | 2013 |
| Efficient verified (UN) SAT certificate checking P Lammich Automated Deduction–CADE 26: 26th International Conference on Automated …, 2017 | 72 | 2017 |
| A verified SAT solver framework with learn, forget, restart, and incrementality JC Blanchette, M Fleury, P Lammich, C Weidenbach Journal of automated reasoning 61, 333-365, 2018 | 71 | 2018 |
| A conference management system with verified document confidentiality S Kanav, P Lammich, A Popescu Computer Aided Verification: 26th International Conference, CAV 2014, Held …, 2014 | 70 | 2014 |
| The Isabelle collections framework P Lammich, A Lochbihler Interactive Theorem Proving: First International Conference, ITP 2010 …, 2010 | 70 | 2010 |
| Applying data refinement for monadic programs to Hopcroft’s algorithm P Lammich, T Tuerk Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012 | 62 | 2012 |
| Predecessor sets of dynamic pushdown networks with tree-regular constraints P Lammich, M Müller-Olm, A Wenner Computer Aided Verification: 21st International Conference, CAV 2009 …, 2009 | 47 | 2009 |
| 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 | 37 | 2018 |
| 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 VMCAI 11, 199-213, 2011 | 37 | 2011 |
| Refinement based verification of imperative data structures P Lammich Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 36 | 2016 |
| Generating verified LLVM from Isabelle/HOL P Lammich 10th International Conference on Interactive Theorem Proving (ITP 2019), 2019 | 35 | 2019 |
| Verified model checking of timed automata S Wimmer, P Lammich Tools and Algorithms for the Construction and Analysis of Systems: 24th …, 2018 | 34 | 2018 |
| Verified efficient implementation of Gabow’s strongly connected component algorithm P Lammich Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as …, 2014 | 34 | 2014 |
| 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 | 34 | 2011 |
| Formal verification of an executable LTL model checker with partial order reduction J Brunner, P Lammich Journal of Automated Reasoning 60, 3-21, 2018 | 28 | 2018 |
| The GRAT tool chain: Efficient (UN) SAT certificate checking with formal correctness guarantees P Lammich Theory and Applications of Satisfiability Testing–SAT 2017: 20th …, 2017 | 27 | 2017 |
| 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 | 27 | 2015 |
| Formalizing the edmonds-karp algorithm P Lammich, SR Sefidgar Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy …, 2016 | 26 | 2016 |
