| A Verified Implementation of B+-Trees in Isabelle/HOL | 0 | 0.34 | 2022 |
| Isabelle'S Metalogic: Formalization And Proof Checker | 0 | 0.34 | 2021 |
| Verification of Closest Pair of Points Algorithms. | 0 | 0.34 | 2020 |
| Verified Textbook Algorithms - A Biased Survey. | 0 | 0.34 | 2020 |
| From LCF to Isabelle/HOL | 0 | 0.34 | 2019 |
| Proof Pearl - Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. | 0 | 0.34 | 2019 |
| Trustworthy Graph Algorithms (Invited Talk). | 0 | 0.34 | 2019 |
| Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra. | 0 | 0.34 | 2019 |
| Weight-Balanced Trees. | 0 | 0.34 | 2018 |
| A Verified Compiler from Isabelle/HOL to CakeML. | 2 | 0.39 | 2018 |
| Optimal Binary Search Trees. | 0 | 0.34 | 2018 |
| Treaps. | 0 | 0.34 | 2018 |
| Propositional Proof Systems. | 0 | 0.34 | 2017 |
| Root-Balanced Tree. | 0 | 0.34 | 2017 |
| Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL. | 2 | 0.37 | 2017 |
| Analysis of List Update Algorithms. | 0 | 0.34 | 2016 |
| Automatic Functional Correctness Proofs For Functional Search Trees | 2 | 0.37 | 2016 |
| Amortized Complexity Verified. | 0 | 0.34 | 2015 |
| Mining the Archive of Formal Proofs | 9 | 0.52 | 2015 |
| A fully verified executable LTL model checker | 28 | 1.17 | 2014 |
| Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions. | 0 | 0.34 | 2014 |
| Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. | 2 | 0.36 | 2013 |
| Deduction and Arithmetic (Dagstuhl Seminar 13411). | 0 | 0.34 | 2013 |
| Verified decision procedures for MSO on words based on derivatives of regular expressions | 0 | 0.34 | 2013 |
| A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions. | 0 | 0.34 | 2013 |
| Data refinement in Isabelle/HOL | 13 | 0.63 | 2013 |
| Formalizing Probabilistic Noninterference | 1 | 0.36 | 2013 |
| Markov Models. | 0 | 0.34 | 2012 |
| A compiled implementation of normalisation by evaluation* | 10 | 0.78 | 2012 |
| Verifying pCTL model checking | 2 | 0.39 | 2012 |
| Proving concurrent noninterference | 1 | 0.35 | 2012 |
| Majority Vote Algorithm Revisited Again. | 0 | 0.34 | 2011 |
| Gauss-Jordan Elimination for Matrices Represented as Functions. | 3 | 0.43 | 2011 |
| Regular Sets and Expressions. | 1 | 0.44 | 2010 |
| Sledgehammer: judgement day | 32 | 1.13 | 2010 |
| List Index. | 0 | 0.34 | 2010 |
| Deduktion: von der Theorie zur Anwendung | 1 | 0.36 | 2010 |
| Code generation via higher-order rewrite systems | 54 | 2.00 | 2010 |
| Linear Quantifier Elimination | 11 | 0.71 | 2010 |
| Social Choice Theory in HOL | 11 | 0.85 | 2009 |
| Proof Synthesis and Reflection for Linear Arithmetic | 8 | 0.66 | 2008 |
| Fun With Tilings. | 0 | 0.34 | 2008 |
| Quantifier Elimination for Linear Arithmetic. | 0 | 0.34 | 2008 |
| The Isabelle Framework | 34 | 1.32 | 2008 |
| Flyspeck II: the basic linear programs | 17 | 1.13 | 2008 |
| Arrow and Gibbard-Satterthwaite. | 0 | 0.34 | 2008 |
| Normalization by Evaluation. | 0 | 0.34 | 2008 |
| Differential dynamic logics: automated theorem proving for hybrid systems | 3 | 0.40 | 2008 |
| Fun With Functions. | 0 | 0.34 | 2008 |
| C++ ist typsicher? Garantiert | 0 | 0.34 | 2007 |
