| Publication | Date of Publication | Type |
|---|
A formalization of the Smith normal form in higher-order logic
Journal of Automated Reasoning | 2022-12-12 | Paper |
Correction to: ``A formalization of the Smith normal form in higher-order logic
Journal of Automated Reasoning | 2022-12-12 | Paper |
A Perron-Frobenius theorem for deciding matrix growth
Journal of Logical and Algebraic Methods in Programming | 2021-11-03 | Paper |
Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
Journal of Automated Reasoning | 2020-11-02 | Paper |
| On the formalization of termination techniques based on multiset orderings | 2020-05-27 | Paper |
| Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL | 2020-05-13 | Paper |
A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
Journal of Automated Reasoning | 2020-04-07 | Paper |
A verified implementation of algebraic numbers in Isabelle/HOL
Journal of Automated Reasoning | 2020-03-03 | Paper |
A verified efficient implementation of the LLL basis reduction algorithm
EPiC Series in Computing | 2019-07-04 | Paper |
| A formalization of the LLL basis reduction algorithm | 2018-10-04 | Paper |
| Foundational (co)datatypes and (co)recursion for higher-order logic | 2018-01-04 | Paper |
| Certifying safety and termination proofs for integer transition systems | 2017-09-22 | Paper |
| AC dependency pairs revisited | 2017-07-19 | Paper |
| Certification of complexity proofs using CeTA | 2017-07-12 | Paper |
Analyzing program termination and complexity automatically with \textsf{AProVE}
Journal of Automated Reasoning | 2017-07-10 | Paper |
Reachability, confluence, and termination analysis with state-compatible automata
Information and Computation | 2017-03-16 | Paper |
Formalizing soundness and completeness of unravelings
Frontiers of Combining Systems | 2017-02-27 | Paper |
| Formalizing Knuth-Bendix orders and Knuth-Bendix completion | 2017-02-01 | Paper |
Algebraic numbers in Isabelle/HOL
Interactive Theorem Proving | 2016-10-27 | Paper |
| A framework for developing stand-alone certifiers | 2016-08-01 | Paper |
Termination Competition (termCOMP 2015)
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Automated termination proofs for logic programs by term rewriting
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Deriving comparators and show functions in Isabelle/HOL
Interactive Theorem Proving | 2015-09-14 | Paper |
Proving termination of programs automatically with AProVE
Automated Reasoning | 2014-09-26 | Paper |
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
Lecture Notes in Computer Science | 2014-07-24 | Paper |
Reachability Analysis with State-Compatible Automata
Language and Automata Theory and Applications | 2014-03-31 | Paper |
Innermost termination of rewrite systems by labeling
Electronic Notes in Theoretical Computer Science | 2014-01-24 | Paper |
Formalizing bounded increase
Interactive Theorem Proving | 2013-08-07 | Paper |
SAT solving for termination proofs with recursive path orders and dependency pairs
Journal of Automated Reasoning | 2013-08-01 | Paper |
Certification of nontermination proofs
Interactive Theorem Proving | 2012-09-20 | Paper |
| Certified subterm criterion and certified usable rules | 2012-04-25 | Paper |
| Modular and certified semantic labeling and unlabeling | 2012-04-24 | Paper |
Generalized and formalized uncurrying
Frontiers of Combining Systems | 2011-10-07 | Paper |
Termination of Isabelle functions via termination of rewriting
Interactive Theorem Proving | 2011-08-17 | Paper |
Signature extensions preserve termination. An alternative proof via dependency pairs
Computer Science Logic | 2010-09-03 | Paper |
Automated termination analysis for logic programs with cut
Theory and Practice of Logic Programming | 2010-08-19 | Paper |
| Improving dependency pairs | 2010-02-24 | Paper |
Certification of Termination Proofs Using CeTA
Lecture Notes in Computer Science | 2009-10-20 | Paper |
Loops under Strategies
Rewriting Techniques and Applications | 2009-06-30 | Paper |
SAT Solving for Termination Analysis with Polynomial Interpretations
Theory and Applications of Satisfiability Testing – SAT 2007 | 2009-03-10 | Paper |
Proving Termination by Bounded Increase
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
From Outermost Termination to Innermost Termination
Lecture Notes in Computer Science | 2009-02-03 | Paper |
Improving Context-Sensitive Dependency Pairs
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
Lecture Notes in Computer Science | 2008-09-25 | Paper |
Proving Termination Using Recursive Path Orders and SAT Solving
Frontiers of Combining Systems | 2008-09-16 | Paper |
Adding constants to string rewriting
Applicable Algebra in Engineering, Communication and Computing | 2008-09-10 | Paper |
Maximal Termination
Rewriting Techniques and Applications | 2008-08-28 | Paper |
Deciding Innermost Loops
Rewriting Techniques and Applications | 2008-08-28 | Paper |
SAT Solving for Argument Filterings
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Automated Termination Analysis for Logic Programs by Term Rewriting
Logic-Based Program Synthesis and Transformation | 2007-09-10 | Paper |
Mechanizing and improving dependency pairs
Journal of Automated Reasoning | 2007-05-03 | Paper |
Frontiers of Combining Systems
Lecture Notes in Computer Science | 2006-10-10 | Paper |
The size-change principle and dependency pairs for termination of term rewriting
Applicable Algebra in Engineering, Communication and Computing | 2005-11-24 | Paper |
Logic for Programming, Artificial Intelligence, and Reasoning
Lecture Notes in Computer Science | 2005-11-10 | Paper |
| scientific article; zbMATH DE number 2043534 (Why is no real title available?) | 2004-02-16 | Paper |
