Christian Sternagel

Publication Activity (10 Years)

Years Active: 2008-2021
Publications (10 Years): 33

Top Topics

Rewrite Systems

Theorem Proving

Reachability Analysis

Link The Wiki Track

Top Venues

Arch. Formal Proofs

Publications

Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel
Regular Tree Relations. Arch. Formal Proofs 2021 (2021)
Christian Sternagel, René Thiemann, Akihisa Yamada
A Formalization of Weighted Path Orders and Recursive Path Orders. Arch. Formal Proofs 2021 (2021)
René Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada
Certifying the Weighted Path Order (Invited Talk). FSCD (2020)
Christian Sternagel, René Thiemann
A Formalization of Knuth-Bendix Orders. Arch. Formal Proofs 2020 (2020)
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
Abstract Completion, Formalized. Log. Methods Comput. Sci. 15 (3) (2019)
Alexander Lochmann, Christian Sternagel
Certified ACKBO. CPP (2019)
Christian Sternagel, Sarah Winkler
Certified Equational Reasoning via Ordered Completion. CADE (2019)
Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada
The Termination and Complexity Competition. TACAS (3) (2019)
Christian Sternagel, Akihisa Yamada
Reachability Analysis for Termination and Confluence of Rewriting. TACAS (1) (2019)
Florian Meßner, Christian Sternagel
nonreach - A Tool for Nonreachability Analysis. TACAS (1) (2019)
Jonas Schöpf, Christian Sternagel
TTT2 with Termination Templates for Teaching. CoRR (2018)
Christian Sternagel
The remote_build Tool. CoRR (2018)
Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel
A Formally Verified Solver for Homogeneous Linear Diophantine Equations. ITP (2018)
Christian Sternagel, René Thiemann
First-Order Terms. Arch. Formal Proofs 2018 (2018)
Christian Sternagel, Sarah Winkler
Certified Ordered Completion. CoRR (2018)
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
Abstract Completion, Formalized. CoRR (2018)
Florian Messner, Julian Parsert, Jonas Schöpf, Christian Sternagel
Homogeneous Linear Diophantine Equations. Arch. Formal Proofs 2017 (2017)
Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel
HOLCF-Prelude. Arch. Formal Proofs 2017 (2017)
Christian Sternagel, Thomas Sternagel
Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. CADE (2017)
Thomas Sternagel, Christian Sternagel
Certified Non-Confluence with ConCon 1.5. CoRR (2017)
Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS (2017)
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
Infinite Runs in Abstract Completion. FSCD (2017)
Christian Sternagel
The Generalized Subterm Criterion in TTT2. CoRR (2016)
Christian Sternagel, Thomas Sternagel
Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion. FSCD (2016)
Akihisa Yamada, Christian Sternagel, René Thiemann, Keiichirou Kusakari
AC Dependency Pairs Revisited. CSL (2016)
Julian Nagele, Vincent van Oostrom, Christian Sternagel
A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle. CoRR (2016)
Christian Sternagel, Thomas Sternagel
Level-Confluence of 3-CTRSs in Isabelle/HOL. CoRR (2016)
Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom, Christian Sternagel
The Z Property. Arch. Formal Proofs 2016 (2016)
Thomas Sternagel, Christian Sternagel
A Characterization of Quasi-Decreasingness. CoRR (2016)
Thomas Sternagel, Christian Sternagel
Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs. CoRR (2016)
Christian Sternagel, René Thiemann
Deriving class instances for datatypes. Arch. Formal Proofs 2015 (2015)
Christian Sternagel, René Thiemann
Deriving Comparators and Show Functions in Isabelle/HOL. ITP (2015)
Martin Avanzini, Christian Sternagel, René Thiemann
Certification of Complexity Proofs using CeTA. RTA (2015)
Christian Sternagel
Certified Kruskal's Tree Theorem. J. Formaliz. Reason. 7 (1) (2014)
Christian Sternagel, René Thiemann
Haskell's Show-Class in Isabelle/HOL. Arch. Formal Proofs 2014 (2014)
Nao Hirokawa, Aart Middeldorp, Christian Sternagel
A New and Formalized Proof of Abstract Completion. ITP (2014)
Christian Sternagel
Imperative Insertion Sort. Arch. Formal Proofs 2014 (2014)
Christian Sternagel, René Thiemann
A Framework for Developing Stand-Alone Certifiers. LSFA (2014)
Christian Sternagel, René Thiemann
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs. RTA-TLCA (2014)
Christian Sternagel, René Thiemann
Certification Monads. Arch. Formal Proofs 2014 (2014)
Christian Sternagel, René Thiemann
XML. Arch. Formal Proofs 2014 (2014)
Christian Sternagel, René Thiemann
The Certification Problem Format. UITP (2014)
Christian Sternagel
Proof Pearl - A Mechanized Proof of GHC's Mergesort. J. Autom. Reason. 51 (4) (2013)
Christian Sternagel, René Thiemann
Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. RTA (2013)
Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel
Certified HLints with Isabelle/HOLCF-Prelude. CoRR (2013)
Christian Sternagel
Certified Kruskal's Tree Theorem. CPP (2013)
Bertram Felgenhauer, Martin Avanzini, Christian Sternagel
A Haskell Library for Term Rewriting. CoRR (2013)
Christian Sternagel
Getting Started with Isabelle/jEdit CoRR (2012)
Christian Sternagel, René Thiemann
Certification of Nontermination Proofs. ITP (2012)
Christian Sternagel, René Thiemann, Sarah Winkler, Harald Zankl
CeTA - A Tool for Certified Termination Analysis CoRR (2012)
Christian Sternagel, René Thiemann
Certification extends Termination Techniques CoRR (2012)
Christian Sternagel, René Thiemann
A Relative Dependency Pair Framework CoRR (2012)
Christian Sternagel
A Locale for Minimal Bad Sequences CoRR (2012)
Christian Sternagel
Well-Quasi-Orders. Arch. Formal Proofs 2012 (2012)
Thomas Sternagel, René Thiemann, Harald Zankl, Christian Sternagel
Recording Completion for Finding and Certifying Proofs in Equational Logic CoRR (2012)
Christian Sternagel
Efficient Mergesort. Arch. Formal Proofs 2011 (2011)
Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl
Termination of Isabelle Functions via Termination of Rewriting. ITP (2011)
Christian Sternagel, René Thiemann
Generalized and Formalized Uncurrying. FroCoS (2011)
Christian Sternagel, René Thiemann
Modular and Certified Semantic Labeling and Unlabeling. RTA (2011)
Christian Sternagel, René Thiemann
Executable Transitive Closures of Finite Relations. Arch. Formal Proofs 2011 (2011)
Christian Sternagel, René Thiemann
Abstract Rewriting. Arch. Formal Proofs 2010 (2010)
Christian Sternagel, René Thiemann
Executable Matrix Operations on Matrices of Arbitrary Dimensions. Arch. Formal Proofs 2010 (2010)
Christian Sternagel, René Thiemann
Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs. CSL (2010)
René Thiemann, Christian Sternagel, Jürgen Giesl, Peter Schneider-Kamp
Loops under Strategies ... Continued IWS (2010)
Christian Sternagel, René Thiemann
Certified Subterm Criterion and Certified Usable Rules. RTA (2010)
Harald Zankl, Christian Sternagel, Dieter Hofbauer, Aart Middeldorp
Finding and Certifying Loops. SOFSEM (2010)
Christian Sternagel, René Thiemann
Executable Multivariate Polynomials. Arch. Formal Proofs 2010 (2010)
Martin Korp, Christian Sternagel, Harald Zankl, Aart Middeldorp
Tyrolean Termination Tool 2. RTA (2009)
René Thiemann, Christian Sternagel
Loops under Strategies. RTA (2009)
René Thiemann, Christian Sternagel
Certification of Termination Proofs Using CeTA. TPHOLs (2009)
Harald Zankl, Christian Sternagel, Aart Middeldorp
Transforming SAT into Termination of Rewriting. Electron. Notes Theor. Comput. Sci. 246 (2009)
Christian Sternagel, Aart Middeldorp
Root-Labeling. RTA (2008)