Root-Labeling. - Christian Sternagel; Aart Middeldorp (RTA, 2008)

Transforming SAT into Termination of Rewriting. - Harald Zankl; Christian Sternagel; Aart Middeldorp (WFLP, 2008)

Tyrolean Termination Tool 2. - Martin Korp; Christian Sternagel; Harald Zankl; Aart Middeldorp (RTA, 2009)

Loops under Strategies. - René Thiemann; Christian Sternagel (RTA, 2009)

Certification of Termination Proofs Using CeTA. - René Thiemann; Christian Sternagel (TPHOLs, 2009)

Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs. - Christian Sternagel; René Thiemann (CSL, 2010)

Certified Subterm Criterion and Certified Usable Rules. - Christian Sternagel; René Thiemann (RTA, 2010)

Finding and Certifying Loops. - Harald Zankl; Christian Sternagel; Dieter Hofbauer; Aart Middeldorp (SOFSEM, 2010)

Abstract Rewriting. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2010)

Executable Matrix Operations on Matrices of Arbitrary Dimensions. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2010)

Executable Multivariate Polynomials. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2010)

Loops under Strategies ... Continued - René Thiemann; Christian Sternagel; Jürgen Giesl; Peter Schneider-Kamp (IWS, 2010)

Generalized and Formalized Uncurrying. - Christian Sternagel; René Thiemann (FroCoS, 2011)

Termination of Isabelle Functions via Termination of Rewriting. - Alexander Krauss 001; Christian Sternagel; René Thiemann; Carsten Fuhs; Jürgen Giesl (ITP, 2011)

Modular and Certified Semantic Labeling and Unlabeling. - Christian Sternagel; René Thiemann (RTA, 2011)

Efficient Mergesort. - Christian Sternagel (Arch. Formal Proofs, 2011)

Executable Transitive Closures of Finite Relations. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2011)

Certification of Nontermination Proofs. - Christian Sternagel; René Thiemann (ITP, 2012)

Well-Quasi-Orders. - Christian Sternagel (Arch. Formal Proofs, 2012)

A Locale for Minimal Bad Sequences - Christian Sternagel (CoRR, 2012)

Getting Started with Isabelle/jEdit - Christian Sternagel (CoRR, 2012)

CeTA - A Tool for Certified Termination Analysis - Christian Sternagel; René Thiemann; Sarah Winkler; Harald Zankl (CoRR, 2012)

Certification extends Termination Techniques - Christian Sternagel; René Thiemann (CoRR, 2012)

A Relative Dependency Pair Framework - Christian Sternagel; René Thiemann (CoRR, 2012)

Recording Completion for Finding and Certifying Proofs in Equational Logic - Thomas Sternagel; René Thiemann; Harald Zankl; Christian Sternagel (CoRR, 2012)

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. - Christian Sternagel; René Thiemann (RTA, 2013)

Certified HLints with Isabelle/HOLCF-Prelude. - Joachim Breitner; Brian Huffman; Neil Mitchell; Christian Sternagel (CoRR, 2013)

A Haskell Library for Term Rewriting. - Bertram Felgenhauer; Martin Avanzini; Christian Sternagel (CoRR, 2013)

Proof Pearl - A Mechanized Proof of GHC's Mergesort. - Christian Sternagel (J. Autom. Reason., 2013)

A New and Formalized Proof of Abstract Completion. - Nao Hirokawa; Aart Middeldorp; Christian Sternagel (ITP, 2014)

Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs. - Christian Sternagel; René Thiemann (RTA-TLCA, 2014)

Imperative Insertion Sort. - Christian Sternagel (Arch. Formal Proofs, 2014)

Haskell's Show-Class in Isabelle/HOL. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2014)

XML. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2014)

Certification Monads. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2014)

The Certification Problem Format. - Christian Sternagel; René Thiemann (UITP, 2014)

A Framework for Developing Stand-Alone Certifiers. - Christian Sternagel; René Thiemann (LSFA, 2014)

Certified Kruskal's Tree Theorem. - Christian Sternagel (J. Formaliz. Reason., 2014)

Deriving Comparators and Show Functions in Isabelle/HOL. - Christian Sternagel; René Thiemann (ITP, 2015)

Certification of Complexity Proofs using CeTA. - Martin Avanzini; Christian Sternagel; René Thiemann (RTA, 2015)

Deriving class instances for datatypes. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2015)

AC Dependency Pairs Revisited. - Akihisa Yamada 002; Christian Sternagel; René Thiemann; Keiichirou Kusakari (CSL, 2016)

Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion. - Christian Sternagel; Thomas Sternagel (FSCD, 2016)

The Z Property. - Bertram Felgenhauer; Julian Nagele; Vincent van Oostrom; Christian Sternagel (Arch. Formal Proofs, 2016)

A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle. - Julian Nagele; Vincent van Oostrom; Christian Sternagel (CoRR, 2016)

The Generalized Subterm Criterion in TTT2. - Christian Sternagel (CoRR, 2016)

Level-Confluence of 3-CTRSs in Isabelle/HOL. - Christian Sternagel; Thomas Sternagel (CoRR, 2016)

Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs. - Thomas Sternagel; Christian Sternagel (CoRR, 2016)

A Characterization of Quasi-Decreasingness. - Thomas Sternagel; Christian Sternagel (CoRR, 2016)

Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. - Christian Sternagel; Thomas Sternagel (CADE, 2017)

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)

Infinite Runs in Abstract Completion. - Nao Hirokawa; Aart Middeldorp; Christian Sternagel; Sarah Winkler (FSCD, 2017)

HOLCF-Prelude. - Joachim Breitner; Brian Huffman; Neil Mitchell; Christian Sternagel (Arch. Formal Proofs, 2017)

Homogeneous Linear Diophantine Equations. - Florian Messner; Julian Parsert; Jonas Schöpf; Christian Sternagel (Arch. Formal Proofs, 2017)

Certified Non-Confluence with ConCon 1.5. - Thomas Sternagel; Christian Sternagel (CoRR, 2017)

A Formally Verified Solver for Homogeneous Linear Diophantine Equations. - Florian Meßner; Julian Parsert; Jonas Schöpf; Christian Sternagel (ITP, 2018)

First-Order Terms. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2018)

The remote_build Tool. - Christian Sternagel (CoRR, 2018)

Certified Ordered Completion. - Christian Sternagel; Sarah Winkler (CoRR, 2018)

TTT2 with Termination Templates for Teaching. - Jonas Schöpf; Christian Sternagel (CoRR, 2018)

Certified Equational Reasoning via Ordered Completion. - Christian Sternagel; Sarah Winkler (CADE, 2019)

Certified ACKBO. - Alexander Lochmann; Christian Sternagel (CPP, 2019)

The Termination and Complexity Competition. - Jürgen Giesl; Albert Rubio; Christian Sternagel; Johannes Waldmann; Akihisa Yamada 002 (TACAS (3), 2019)

nonreach - A Tool for Nonreachability Analysis. - Florian Meßner; Christian Sternagel (TACAS (1), 2019)

Reachability Analysis for Termination and Confluence of Rewriting. - Christian Sternagel; Akihisa Yamada 002 (TACAS (1), 2019)

Abstract Completion, Formalized. - Nao Hirokawa; Aart Middeldorp; Christian Sternagel; Sarah Winkler (Log. Methods Comput. Sci., 2019)

Certifying the Weighted Path Order (Invited Talk). - René Thiemann; Jonas Schöpf; Christian Sternagel; Akihisa Yamada 002 (FSCD, 2020)

A Formalization of Knuth-Bendix Orders. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2020)

Regular Tree Relations. - Alexander Lochmann; Bertram Felgenhauer; Christian Sternagel; René Thiemann; Thomas Sternagel (Arch. Formal Proofs, 2021)

A Formalization of Weighted Path Orders and Recursive Path Orders. - Christian Sternagel; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2021)

First-Order Rewriting. - René Thiemann; Christian Sternagel; Christina Kirk; Martin Avanzini; Bertram Felgenhauer; Julian Nagele; Thomas Sternagel; Sarah Winkler; Akihisa Yamada 002 (Arch. Formal Proofs, 2025)