René Thiemann

Arch. Formal Proofs, 2024

Verifying a Decision Procedure for Pattern Completeness.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

Undecidability Results on Orienting Single Rewrite Rules.

[BibT_eX]

[DOI]

Fabian Mitterwallner

Arch. Formal Proofs, 2024

A Preprocessor for Linear Diophantine Equalities and Inequalities.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

Linear Termination is Undecidable.

[BibT_eX]

[DOI]

Fabian Mitterwallner

Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 2024

A Verified Algorithm for Deciding Pattern Completeness.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs.

[BibT_eX]

[DOI]

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

Linear Termination over N is Undecidable.

[BibT_eX]

[DOI]

Fabian Mitterwallner

CoRR, 2023

A Verified Efficient Implementation of the Weighted Path Order.

[BibT_eX]

[DOI]

Elias Wenninger

Arch. Formal Proofs, 2023

2022

Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic.

[BibT_eX]

[DOI]

J. Autom. Reason., 2022

A Formalization of the Smith Normal Form in Higher-Order Logic.

[BibT_eX]

[DOI]

J. Autom. Reason., 2022

The Generalized Multiset Ordering is NP-Complete.

[BibT_eX]

[DOI]

Lukas Schmidinger

Arch. Formal Proofs, 2022

Clique is not solvable by monotone circuits of polynomial size.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2022

Duality of Linear Programming.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2022

A Verified Translation of Multitape Turing Machines into Singletape Turing Machines.

[BibT_eX]

[DOI]

Christian Dalvit

Arch. Formal Proofs, 2022

2021

A Perron-Frobenius theorem for deciding matrix growth.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2021

Solving Cubic and Quartic Equations.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

The Sunflower Lemma of Erdős and Rado.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

A Formalization of Weighted Path Orders and Recursive Path Orders.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Regular Tree Relations.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Factorization of Polynomials with Algebraic Coefficients.

[BibT_eX]

[DOI]

Manuel Eberl

Arch. Formal Proofs, 2021

Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

An Isabelle/HOL formalization of AProVE's termination method for LLVM IR.

[BibT_eX]

[DOI]

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

A Verified Implementation of Algebraic Numbers in Isabelle/HOL.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

A Formalization of Knuth-Bendix Orders.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 12th International Symposium, 2020

Certifying the Weighted Path Order (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

2019

Logical and Semantic Frameworks with Applications.

[BibT_eX]

[DOI]

Vivek Nigam

Theor. Comput. Sci., 2019

Linear Inequalities.

[BibT_eX]

[DOI]

Alban Reynaud

Arch. Formal Proofs, 2019

Farkas' Lemma and Motzkin's Transposition Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2019

Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

2018

First-Order Terms.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

An Incremental Simplex Algorithm with Unsatisfiable Core Generation.

[BibT_eX]

[DOI]

Filip Maric

Mirko Spasic

Arch. Formal Proofs, 2018

A verified factorization algorithm for integer polynomials with polynomial complexity.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

A verified LLL algorithm.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

Extending a Verified Simplex Algorithm.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22 Workshop and Short Paper Proceedings, 2018

A Verified Efficient Implementation of the LLL Basis Reduction Algorithm.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

A Formalization of the LLL Basis Reduction Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper).

[BibT_eX]

[DOI]

Ondrej Kuncar

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

Analyzing Program Termination and Complexity Automatically with AProVE.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

Reachability, confluence, and termination analysis with state-compatible automata.

[BibT_eX]

[DOI]

Bertram Felgenhauer

Inf. Comput., 2017

Stochastic Matrices and the Perron-Frobenius Theorem.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Subresultants.

[BibT_eX]

[DOI]

Jasmin Christian Blanchette

Arch. Formal Proofs, 2017

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.

[BibT_eX]

[DOI]

Julian Biendarra

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

A formalization of the Berlekamp-Zassenhaus factorization algorithm.

[BibT_eX]

[DOI]

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

Certifying Safety and Termination Proofs for Integer Transition Systems.

[BibT_eX]

[DOI]

Marc Brockschmidt

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Polynomial Interpolation.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Polynomial Factorization.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Perron-Frobenius Theorem for Spectral Radius Analysis.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

The Factorization Algorithm of Berlekamp and Zassenhaus.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

AC Dependency Pairs Revisited.

[BibT_eX]

[DOI]

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

Formalizing jordan normal forms in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015

Preface.

[BibT_eX]

[DOI]

Mario R. F. Benevides

Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

Certification of Confluence Proofs using CeTA.

[BibT_eX]

[DOI]

Julian Nagele

CoRR, 2015

Matrices, Jordan Normal Forms, and Spectral Radius Theory.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

Algebraic Numbers in Isabelle/HOL.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

Deriving class instances for datatypes.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

Certification of Complexity Proofs using CeTA.

[BibT_eX]

[DOI]

Martin Avanzini

Proceedings of the 26th International Conference on Rewriting Techniques and Applications, 2015

Deriving Comparators and Show Functions in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Formalizing Soundness and Completeness of Unravelings.

[BibT_eX]

[DOI]

Sarah Winkler

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Termination Competition (termCOMP 2015).

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

2014

A Framework for Developing Stand-Alone Certifiers.

[BibT_eX]

[DOI]

Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

The Certification Problem Format.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, 2014

Lifting Definition Option.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Mutually Recursive Partial Functions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Implementing field extensions of the form Q[sqrt(b)].

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Certification Monads.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

XML.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Haskell's Show-Class in Isabelle/HOL.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations.

[BibT_eX]

[DOI]

Julian Nagele

Sarah Winkler

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs.

[BibT_eX]

[DOI]

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Reachability Analysis with State-Compatible Automata.

[BibT_eX]

[DOI]

Bertram Felgenhauer

Proceedings of the Language and Automata Theory and Applications, 2014

Proving Termination of Programs Automatically with AProVE.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Computing Square Roots using the Babylonian Method.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2013

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion.

[BibT_eX]

[DOI]

Proceedings of the 24th International Conference on Rewriting Techniques and Applications, 2013

Formalizing Bounded Increase.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

Towards the Certification of Complexity Proofs

[BibT_eX]

[DOI]

CoRR, 2012

Recording Completion for Finding and Certifying Proofs in Equational Logic

[BibT_eX]

[DOI]

CoRR, 2012

A Relative Dependency Pair Framework

[BibT_eX]

[DOI]

CoRR, 2012

Certification extends Termination Techniques

[BibT_eX]

[DOI]

CoRR, 2012

CeTA - A Tool for Certified Termination Analysis

[BibT_eX]

[DOI]

CoRR, 2012

Generating linear orders for datatypes.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2012

Executable Transitive Closures.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2012

On the Formalization of Termination Techniques based on Multiset Orderings.

[BibT_eX]

[DOI]

Guillaume Allais

Julian Nagele

Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , 2012

Certification of Nontermination Proofs.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

Automated termination proofs for haskell by term rewriting.

[BibT_eX]

[DOI]

Matthias Raffelsieper

Stephan Swiderski

ACM Trans. Program. Lang. Syst., 2011

Executable Transitive Closures of Finite Relations.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2011

Modular and Certified Semantic Labeling and Unlabeling.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Termination of Isabelle Functions via Termination of Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Generalized and Formalized Uncurrying.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

2010

Automated termination analysis for logic programs with cut.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2010

Loops under Strategies ... Continued

[BibT_eX]

[DOI]

Proceedings of the Proceedings International Workshop on Strategies in Rewriting, 2010

Executable Multivariate Polynomials.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2010

Executable Matrix Operations on Matrices of Arbitrary Dimensions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2010

Abstract Rewriting.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2010

Certified Subterm Criterion and Certified Usable Rules.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Rewriting Techniques and Applications, 2010

Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009

Automated termination proofs for logic programs by term rewriting.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2009

Certification of Termination Proofs Using CeTA.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

From Outermost Termination to Innermost Termination.

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2009: Theory and Practice of Computer Science, 2009

Loops under Strategies.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 20th International Conference, 2009

2008

Is our self based on reward? Self-relatedness recruits neural activity in the reward system.

[BibT_eX]

[DOI]

NeuroImage, 2008

Adding constants to string rewriting.

[BibT_eX]

[DOI]

Appl. Algebra Eng. Commun. Comput., 2008

Deciding Innermost Loops.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Maximal Termination.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Improving Context-Sensitive Dependency Pairs.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

2007

The DP framework for proving termination of term rewriting.

[BibT_eX]

[DOI]

PhD thesis, 2007

Innermost Termination of Rewrite Systems by Labeling.

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming, 2007

SAT Solving for Termination Analysis with Polynomial Interpretations.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Proving Termination Using Recursive Path Orders and SAT Solving.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 6th International Symposium, 2007

Decision Procedures for Loop Detection.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Implementing RPO and POLO using SAT.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Termination of Programs using Term Rewriting and SAT Solving.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Proving Termination by Bounded Increase.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

2006

Mechanizing and Improving Dependency Pairs.

[BibT_eX]

[DOI]

J. Autom. Reason., 2006

Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

SAT Solving for Argument Filterings.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

Automated Termination Analysis for Logic Programs by Term Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2006

Automatic Termination Proofs in the Dependency Pair Framework.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

The size-change principle and dependency pairs for termination of term rewriting.

[BibT_eX]

[DOI]

Appl. Algebra Eng. Commun. Comput., 2005

Proving and Disproving Termination of Higher-Order Functions.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

Proving and Disproving Termination in the Dependency Pair Framework.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

2004

Automated Termination Proofs with AProVE.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 15th International Conference, 2004

The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

Improved Modular Termination Proofs Using Dependency Pairs.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

Size-Change Termination for Term Rewriting.

[BibT_eX]

[DOI]