M. W. Haslbeck and R. Thiemann

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

In *Proceedings of the 10th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '21)*,
pages 238 - 249, 2021.

R. Bottesch, M. W. Haslbeck, A. Reynaud and R. Thiemann

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

In *Proceedings of the 12th International NASA Formal Methods Symposium (NFM '20)*,
Lecture Notes in Computer Science 12229, pages 233 - 250, 2020.

R. Thiemann, J. Schöpf, C. Sternagel, and A. Yamada

Certifying the Weighted Path Order

In *Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD '20)*,
Leibniz International Proceedings in Informatics 167, pages 4:1 - 4:20, 2020.

R. Bottesch, M. W. Haslbeck, and R. Thiemann.

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

In *Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS '19)*,
Lecture Notes in Computer Science 11715, pages 223 – 239, 2019.

R. Bottesch, M. W. Haslbeck, and R. Thiemann.

A Verified Efficient Implementation of the LLL Basis Reduction Algorithm

In *Proceedings of the 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR '18)*,
EPiC Series in Computing 57, pages 164 – 180, 2018.

J. Divasón, S. Joosten, R. Thiemann, and A. Yamada.

A Formalization of the LLL Basis Reduction Algorithm

In *Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP '18)*,
Lecture Notes in Computer Science 10895, pages 160-177, 2018.

J. Divasón, S. Joosten, O. Kunčar, R. Thiemann, and A. Yamada.

Efficient Certification of Complexity Proofs – Formalizing the Perron-Frobenius Theorem

In *Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '18)*,
pages 2-13, 2018.

J. Biendarra, J. Blanchette, A. Bouzy, M. Desharnais, M. Fleury, J. Hölzl, O. Kunčar, A. Lochbihler, F. Meier, L. Panny, A. Popescu, C. Sternagel, R. Thiemann, and D. Traytel.

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

In *Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS '17)*,
Lecture Notes in Computer Science 10483, pages 3-21, 2017.

M. Brockschmidt, S. Joosten, R. Thiemann, and A. Yamada.

Certifying Safety and Termination Proofs for Integer Transition Systems

In *Proceedings of the 26th International Conference on Automated Deduction (CADE '17)*,
Lecture Notes in Computer Science 10395, pages 454-471, 2017.

J. Divasón, S. Joosten, R. Thiemann, and A. Yamada.

A Formalization of the Berlekamp–Zassenhaus Factorization Algorithm

In *Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '17)*,
pages 17-29, 2017.

Akihisa Yamada, C. Sternagel, R. Thieman, and K. Kusakari

AC Dependency Pairs Revisited

In *Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL '16)*,
Leibniz International Proceedings in Informatics 62, pages 8:1-8:16, 2016.

R. Thiemann and A. Yamada.

Algebraic Numbers in Isabelle/HOL

In *Proceedings of the 7th International Conference on
Interactive Theorem Proving (ITP '16)*,
Lecture Notes in Computer Science 9807, pages 391-408, 2016.

R. Thiemann and A. Yamada.

Formalizing Jordan Normal Forms in Isabelle/HOL

In *Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '16)*,
pages 88-99, 2016.

S. Winkler and R. Thiemann.

Formalizing Soundness and Completeness of Unravelings

In *Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS '15)*,
Lecture Notes in Artificial Intelligence 9322, pages 239-255, 2015.

C. Sternagel and R. Thiemann.

Deriving Comparators and Show Functions in Isabelle/HOL

In *Proceedings of the 6th International Conference on
Interactive Theorem Proving (ITP '15)*,
Lecture Notes in Computer Science 9236, pages 421-437, 2015.

M. Avanzini, C. Sternagel, and R. Thiemann

Certification of Complexity Proofs using CeTA

In *Proceedings of the Joint 26th International Conference on
Rewriting Techniques and Applications (RTA '15)*,
Leibniz International Proceedings in Informatics 36, pages 23-39, 2015.

J. Nagele, R. Thiemann, and S. Winkler

Certification of Nontermination Proofs using Strategies and Nonlooping Derivations

In *Proceedings of the 6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '14)*,
Lecture Notes in Computer Science, 8471, pages 216-232, 2014,
© Springer-Verlag.

C. Sternagel and R. Thiemann

The Certification Problem Format

In *Proceedings of the 11th International Workshop on User Interfaces for Theorem Provers (UITP '14)*,
Electronic Proceedings in Theoretical Computer Science 167:61-72, 2014.

J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto,
M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann

Proving Termination of Programs Automatically with AProVE

In *Proceedings of the 7th International Joint Conference on Automated
Reasoning (IJCAR '14)*,
Lecture Notes in Computer Science, 8562, pages 184-191, 2014,
© Springer-Verlag.

C. Sternagel and R. Thiemann

Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs

In *Proceedings of the Joint 25th International Conference on
Rewriting Techniques and Applications
and 12th International Conference on
Typed Lambda Calculi and Applications (RTA-TLCA '14)*,
Lecture Notes in Computer Science 8560 (Advanced Research in Computing and Software Science), pages 441-455, 2014,
© Springer-Verlag.

B. Felgenhauer and R. Thiemann.

Reachability Analysis with State-Compatible Automata

In *Proceedings of 8th International Conference on Language and Automata Theory and Applications (LATA '14)*,
Lecture Notes in Computer Science 8370, pages 347-359, 2014, ©
Springer-Verlag.

R. Thiemann.

Formalizing Bounded Increase

In *Proceedings of the 4th International Conference on
Interactive Theorem Proving (ITP '13)*,
Lecture Notes in Computer Science 7998, pages 245-260, 2013, ©
Springer-Verlag.

C. Sternagel and R. Thiemann.

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion

In *Proceedings of the 24th International Conference on
Rewriting Techniques and Applications (RTA '13)*,
Leibniz International Proceedings in Informatics 21:287-302, 2013.

C. Sternagel and R. Thiemann.

Certification of Nontermination Proofs

In *Proceedings of the 3rd International Conference on
Interactive Theorem Proving (ITP '12)*,
Lecture Notes in Computer Science 7406, pages 266-282, 2012, ©
Springer-Verlag.

R. Thiemann, G. Allais, and J. Nagele.

On the formalization of termination techniques based on multiset orderings

In *Proceedings of the 23rd International Conference on
Rewriting Techniques and Applications (RTA '12)*,
Leibniz International Proceedings in Informatics 15:339-354, 2012.

C. Sternagel and R. Thiemann.

Generalized and Formalized Uncurrying

In *Proceedings of the 8th International Symposium Frontiers of Combining Systems (FroCoS '11)*,
Lecture Notes in Artificial Intelligence 6989, pages 243-258, 2011. ©
Springer-Verlag.

A. Krauss, C. Sternagel, R. Thiemann, C. Fuhs, and J. Giesl.

Termination of Isabelle Functions via Termination of Rewriting

In *Proceedings of the 2nd International Conference on
Interactive Theorem Proving (ITP '11)*,
Lecture Notes in Computer Science 6898, pages 152-167, 2011. ©
Springer-Verlag.

C. Sternagel and R. Thiemann

Modular and certified semantic labeling and unlabeling

In *Proceedings of the 22nd International Conference on
Rewriting Techniques and Applications (RTA '11)*,
Leibniz International Proceedings in Informatics 10:329-344, 2011.

R. Thiemann, C. Sternagel, J. Giesl, and P. Schneider-Kamp

Loops under Strategies ... Continued

In *Proceedings of the International Workshop on
Strategies in Rewriting, Proving, and Programming*, Electronic Proceedings in Theoretical Computer Science 44:51-65, 2010.

C. Sternagel and R. Thiemann

Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs

In *Proceedings of the 19th EACSL Annual Conferences on Computer Science Logic (CSL '10)*,
Lecture Notes in Computer Science 6247, pages 514-528, 2010. ©
Springer-Verlag.

P. Schneider-Kamp, J. Giesl, T. Ströder, A. Serebrenik, and R. Thiemann

Automated termination analysis for logic programs with cut

In *Proceedings of the 26th International Conference on Logic Programming (ICLP '10)*, *Theory and Practice of Logic Programming* 10(4-6):365-381, 2010.

Cambridge University Press.

Extended version appeared as Technical Report AIB-2010-10, RWTH Aachen, Germany.

C. Sternagel and R. Thiemann

Certified Subterm Criterion and Certified Usable Rules

In *Proceedings of the 21st International Conference on
Rewriting Techniques and Applications (RTA '10)*,
Leibniz International Proceedings in Informatics 6:325-340, 2010.

R. Thiemann and C. Sternagel

Certification of Termination Proofs using CeTA

In *Proceedings of the 22nd International Conference on
Theorem Proving in Higher Order Logics (TPHOLs '09)*, Lecture Notes in Computer Science 5674, pages 452-468, 2009. ©
Springer-Verlag.

R. Thiemann and C. Sternagel

Loops under Strategies

In *Proceedings of the 20th International Conference on
Rewriting Techniques and Applications (RTA '09)*, Lecture Notes in Computer Science 5595, pages 17-31, 2009. ©
Springer-Verlag.

All proofs are available in this extended version.

R. Thiemann

From outermost termination to innermost termination

In *Proceedings of the 35th Conference on
Current Trends in Theory and Practice of Computer Science (SOFSEM '09)*,
Spindleruv Mlyn, Czech Republic. Lecture Notes in Computer Science 5404, pages 533-545, 2009. © Springer-Verlag

B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutierrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann

Improving Context-Sensitive Dependency Pairs

In *Proceedings of the 15th International Conference on
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '08)*, Doha, Qatar, Lecture Notes in Computer Science 5330, pages 636-651, 2008. ©
Springer-Verlag.

Extended version available as Technical Report AIB-2008-13, RWTH Aachen, Germany.

R. Thiemann, J. Giesl, and P. Schneider-Kamp

Deciding Innermost Loops

In *Proceedings of the 19th International Conference on
Rewriting Techniques and Applications (RTA '08)*, Hagenberg, Austria, Lecture Notes in Computer Science 5117, pages 366-380, 2008. ©
Springer-Verlag

C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl

Maximal Termination

In *Proceedings of the 19th International Conference on
Rewriting Techniques and Applications (RTA '08)*, Hagenberg, Austria, Lecture Notes in Computer Science 5117, pages 110-125, 2008. ©
Springer-Verlag

Extended version available as Technical Report AIB-2008-03, RWTH Aachen, Germany.

R. Thiemann and A. Middeldorp

Innermost Termination of Rewrite Systems by Labeling

In *Proceedings of the 7th International Workshop on Reduction
Strategies in Rewriting and Programming (WRS '07)*, Paris, France,
Electronic Notes in Theoretical Computer Science 204 (2008), pages 3-19, 2008. ©
Elsevier.

Original publication available at Science Direct.

P. Schneider-Kamp, R. Thiemann, E. Annov, M. Codish, and J. Giesl

Proving Termination using Recursive Path Orders and SAT Solving

In *Proceedings of the 6th International Symposium on Frontiers of Combining Systems
(FroCoS '07)*,
Liverpool, UK, Lecture Notes in Artificial Intelligence 4720,
pages 267-282, 2007. ©
Springer-Verlag

J. Giesl, R. Thiemann, S. Swiderski, and P. Schneider-Kamp

Proving Termination by Bounded Increase

In *Proceedings of the 21st Conference on Automated Deduction (CADE '07)*, Bremen, Germany,
Lecture Notes in Artificial Intelligence 4603, pages 443-459, 2007. ©Springer-Verlag

C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl

SAT Solving for Termination Analysis with Polynomial Interpretations

In *Proceedings of the 10th International Conference on
Theory and Applications of Satisfiability Testing (SAT '07)*, Lisbon, Portugal,
Lecture Notes in Computer Science 4501, pages 340-354, 2007. ©Springer-Verlag

P. Schneider-Kamp, J. Giesl, A. Serebrenik, and R. Thiemann

Automated Termination Analysis for Logic Programs by Term Rewriting

In *Proceedings of the 16th International Symposium on Logic-Based Program
Synthesis and Transformation (LOPSTR '06)*, Venice, Italy, Lecture
Notes in Computer Science 4407, pages 177-193, 2006. ©Springer-Verlag

M. Codish, P. Schneider-Kamp, V. Lagoon, R. Thiemann, and J. Giesl

SAT Solving for Argument Filterings

In *Proceedings of the 13th International Conference on Logic for
Programming, Artificial Intelligence, and Reasoning (LPAR '06)*,
Phnom Penh, Cambodia, Lecture Notes in Artificial Intelligence 4246, pages 30-44, 2006. ©
Springer-Verlag

J. Giesl, P. Schneider-Kamp, and R. Thiemann

AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework

In *Proceedings of the 3rd International Joint Conference on Automated
Reasoning (IJCAR '06)*, Seattle, USA, Lecture
Notes in Artificial Intelligence 4130, pages 281-286, 2006. ©Springer-Verlag

J. Giesl, S. Swiderski, P. Schneider-Kamp, and R. Thiemann

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

In *Proceedings of the 17th International Conference on Rewriting
Techniques and Applications (RTA '06)*, Seattle, USA, Lecture
Notes in Computer Science 4098, pages 297-312, 2006. ©Springer-Verlag

J. Giesl, R. Thiemann, and P. Schneider-Kamp

Proving and Disproving Termination of Higher-Order Functions

In *Proceedings of the 5th International Workshop on Frontiers of
Combining Systems (FroCoS '05)*,
Vienna, Austria, Lecture Notes in Artificial Intelligence 3717,
pages 216-231, 2005. ©
Springer-Verlag

J. Giesl, R. Thiemann, and P. Schneider-Kamp

The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs

In *Proceedings of the 11th International Conference on Logic for
Programming, Artificial Intelligence, and Reasoning (LPAR '04)*,
Montevideo, Uruguay, Lecture Notes in Artificial Intelligence 3452,
pages 301-331, 2005. ©
Springer-Verlag

R. Thiemann, J. Giesl, and P. Schneider-Kamp

Improved Modular Termination Proofs Using Dependency Pairs

In *Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR '04)*,
Cork, Ireland, Lecture Notes in Artificial Intelligence 3097, pages 75-90, 2004.
©
Springer-Verlag

J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke

Automated Termination Proofs with AProVE

In *Proceedings of the 15th International Conference
on Rewriting Techniques and Applications (RTA '04)*,
Aachen, Germany, Lecture Notes in Computer Science 3091, pages 210-220, 2004.
©
Springer-Verlag

J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke

Improving Dependency Pairs

In *Proceedings of the 10th International Conference on Logic for
Programming, Artificial Intelligence, and Reasoning (LPAR '03)*,
Almaty, Kazakhstan, Lecture Notes in Artificial Intelligence 2850, pages 167-182, 2003.
©Springer-Verlag

Extended version available as Technical Report AIB-2003-04, RWTH Aachen, Germany.

R. Thiemann and J. Giesl

Size-Change Termination for Term Rewriting

In *Proceedings of the 14th International Conference on Rewriting
Techniques and Applications (RTA '03)*, Valencia, Spain,
Lecture
Notes in Computer Science 2706, pages 264-278, 2003.
©Springer-Verlag

Extended version available as Technical Report AIB-2003-02, RWTH Aachen, Germany.