| Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic. | 0 | 0.34 | 2022 |
| A Formalization of the Smith Normal Form in Higher-Order Logic. | 0 | 0.34 | 2022 |
| A Perron–Frobenius theorem for deciding matrix growth | 0 | 0.34 | 2021 |
| A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm | 0 | 0.34 | 2020 |
| A Verified Implementation of Algebraic Numbers in Isabelle/HOL | 0 | 0.34 | 2020 |
| Certifying the Weighted Path Order (Invited Talk). | 0 | 0.34 | 2020 |
| Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL. | 0 | 0.34 | 2020 |
| Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. | 0 | 0.34 | 2020 |
| Farkas' Lemma and Motzkin's Transposition Theorem. | 0 | 0.34 | 2019 |
| Logical and Semantic Frameworks with Applications | 0 | 0.34 | 2019 |
| Linear Inequalities. | 0 | 0.34 | 2019 |
| Extending a Verified Simplex Algorithm. | 0 | 0.34 | 2018 |
| Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). | 0 | 0.34 | 2018 |
| A verified LLL algorithm. | 0 | 0.34 | 2018 |
| First-Order Terms. | 0 | 0.34 | 2018 |
| A verified factorization algorithm for integer polynomials with polynomial complexity. | 0 | 0.34 | 2018 |
| An Incremental Simplex Algorithm with Unsatisfiable Core Generation. | 0 | 0.34 | 2018 |
| A Verified Efficient Implementation of the LLL Basis Reduction Algorithm. | 0 | 0.34 | 2018 |
| Certifying Safety and Termination Proofs for Integer Transition Systems. | 1 | 0.35 | 2017 |
| Analyzing Program Termination and Complexity Automatically with AProVE. | 23 | 0.77 | 2017 |
| Stochastic Matrices and the Perron-Frobenius Theorem. | 0 | 0.34 | 2017 |
| Reachability, confluence, and termination analysis with state-compatible automata. | 0 | 0.34 | 2017 |
| Subresultants. | 0 | 0.34 | 2017 |
| Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. | 1 | 0.37 | 2017 |
| A formalization of the Berlekamp-Zassenhaus factorization algorithm. | 3 | 0.42 | 2017 |
| Perron-Frobenius Theorem for Spectral Radius Analysis. | 0 | 0.34 | 2016 |
| Algebraic Numbers In Isabelle/Hol | 0 | 0.34 | 2016 |
| Formalizing jordan normal forms in Isabelle/HOL. | 6 | 0.52 | 2016 |
| AC Dependency Pairs Revisited. | 0 | 0.34 | 2016 |
| The Factorization Algorithm of Berlekamp and Zassenhaus. | 0 | 0.34 | 2016 |
| Polynomial Interpolation. | 0 | 0.34 | 2016 |
| Polynomial Factorization. | 0 | 0.34 | 2016 |
| Certification of Complexity Proofs using CeTA. | 4 | 0.51 | 2015 |
| Matrices, Jordan Normal Forms, and Spectral Radius Theory. | 2 | 0.38 | 2015 |
| Certification of Confluence Proofs using CeTA | 3 | 0.39 | 2015 |
| Formalizing Soundness and Completeness of Unravelings. | 1 | 0.35 | 2015 |
| Termination Competition (termCOMP 2015) | 3 | 0.48 | 2015 |
| Deriving class instances for datatypes. | 1 | 0.35 | 2015 |
| Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs. | 3 | 0.39 | 2014 |
| Mutually Recursive Partial Functions. | 1 | 0.35 | 2014 |
| Lifting Definition Option. | 0 | 0.34 | 2014 |
| Implementing field extensions of the form Q[sqrt(b)]. | 1 | 0.35 | 2014 |
| Proving Termination of Programs Automatically with AProVE. | 38 | 1.27 | 2014 |
| Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations. | 0 | 0.34 | 2014 |
| Certification Monads. | 0 | 0.34 | 2014 |
| XML. | 0 | 0.34 | 2014 |
| Reachability Analysis with State-Compatible Automata. | 7 | 0.56 | 2014 |
| Haskell's Show-Class in Isabelle/HOL. | 0 | 0.34 | 2014 |
| Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. | 7 | 0.49 | 2013 |
| Computing Square Roots using the Babylonian Method. | 0 | 0.34 | 2013 |
