Certification Redux

Term rewriting is a simple yet powerful model of computation that underlies much of declarative programming and computer assisted theorem proving. Moreover, there are methods to reduce verification tasks of computer programs to ensuring properties of corresponding term rewrite systems. Confluence and termination are arguably the most important properties of term rewriting. While termination states that all computation paths yield a result (thereby making sure that we do not have to wait indefinitely to obtain a result), confluence guarantees that computations are deterministic in the sense that any two computation paths can be joined eventually. Together, termination and confluence imply that independent of the strategy used to compute results, we will always obtain the same result for the same input. Thus, terminating and confluent systems of rewrite rules are of special interest, since they yield decision procedures for their respective equational theories (i.e., equality of two terms modulo a set of equations can be decided by rewriting them both exhaustively and comparing the results). Completion provides a way of transforming a given set of equations into an equivalent set of rewrite rules that is terminating and confluent. In the recent past, certification is very successful in the area of automated termination and confluence proving as well as completion. Where by certification we mean the automatic and reliable verification of proofs that were generated by some untrusted tool (e.g., an automatic termination, confluence, or completion tool). In certification the predominant approach is separated into two stages: First formalize the underlying theory and techniques that are used by untrusted tools with the help of a proof assistant (e.g., Isabelle/HOL). Then, given a proof that was generated by such an untrusted tool, check whether all employed techniques where applied correctly. In the first stage we make sure that the mathematical basis of all used techniques is sound in general and that no implicit assumptions are missing; whereas in the second one their correct application on specific problems is verified rigorously. One of the available certifiers is our tool CeTA, which is code generated from our Isabelle Formalization of Rewriting (IsaFoR), an Isabelle/HOL library that contains many results on rewriting. As our main project goals we strive to extend IsaFoR and CeTA as follows: (1) Add a formalization of the recently introduced weighted path order (WPO). Furthermore, adapt WPO to rewriting modulo associativity and commutativity (AC-rewriting). (2) Support certification of conditional confluence proofs by CeTA. (3) Formalize the theory of AC-rewriting, AC-unification, and normalized completion in order to support certification of normalized completion proofs by CeTA. This will bring CeTA up to speed with the most recent tool developments of termination tools, confluence tools, and completion tools.

project start: February 2015
original project end: January 2018
extended until January 2019

Members

• Alexander Lochmann
• Florian Meßner
• Julian Parsert
• Jonas Schöpf
• Christian Sternagel (coordination)
• Thomas Sternagel
• Akihisa Yamada

FWF project number

Contact

Publications

A Formalization of Weighted Path Orders and Recursive Path Orders
Christian Sternagel, René Thiemann, Akihisa Yamada
Archive of Formal Proofs 2021.

Certifying the Weighted Path Order
Rene Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 4:1 – 4:20, 2020.

A Formalization of Knuth-Bendix Orders
Christian Sternagel, René Thiemann
Archive of Formal Proofs 2020.

Abstract Completion, Formalized
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
Logical Methods in Computer Science,  15(3), pp. 19:1 – 19:42, 2019.

Certified Equational Reasoning via Ordered Completion
Christian Sternagel and Sarah Winkler
27th International Conference on Automated Deduction, Lecture Notes in Computer Science 11716, pp. 508 – 525, 2019.

Reachability Analysis for Termination and Confluence of Rewriting
Christian Sternagel, Akihisa Yamada
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 11427, pp. 262 – 278, 2019.

The Termination and Complexity Competition
Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 11429, pp. 155 – 166, 2019.

nonreach – A Tool for Nonreachability Analysis
Florian Meßner, Christian Sternagel
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 11427, pp. 337 – 343, 2019.

Certified ACKBO
Alexander Lochmann, Christian Sternagel
8th ACM SIGPLAN International Conference on Certified Programs and Proofs,   pp. 144 – 151, 2019.

TermComp 2018 Participant: TTT2
Florian Meßner, Christian Sternagel
Proceedings of the 16th International Workshop on Termination (WST 2018),   pp. 79, 2018.

CoCo 2018 Participant: ConCon 1.5
Thomas Sternagel, Christian Sternagel, Aart Middeldorp
Proceedings of the 7th International Workshop on Confluence (IWC 2018),   pp. 66, 2018.

TTT2 with Termination Templates for Teaching
Jonas Schöpf, Christian Sternagel
Proceedings of the 16th International Workshop on Termination (WST 2018),  2018.

Certified Ordered Completion
Christian Sternagel, Sarah Winkler
Proceedings of the 7th International Workshop on Confluence (IWC 2018),  2018.

The remote_build Tool
Christian Sternagel
Isabelle Workshop (Isabelle 2018),  2018.

CoCo 2018 Participant: CeTA 2.33
Bertram Felgenhauer, Franziska Rapp, Christian Sternagel and Sarah Winkler
Proceedings of the 7th International Workshop on Confluence (IWC 2018),   pp. 63, 2018.

A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel
9th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 441 – 458, 2018.

First-Order Terms
Christian Sternagel, René Thiemann
Archive of Formal Proofs,  2018.

Reliable Confluence Analysis of Conditional Term Rewrite Systems
Thomas Sternagel
PhD thesis, University of Innsbruck, 2017.

Homogeneous Linear Diophantine Equations
Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel
The Archive of Formal Proofs,  2017.

Certified Non-Confluence with ConCon 1.5
Thomas Sternagel, Christian Sternagel
Proceedings of the 6th International Workshop on Confluence (IWC 2017),  2017.

Formalized Ground Completion
Aart Middeldorp and Christian Sternagel
Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 51 – 55, 2017.

CoCo 2017 Participant: CeTA 2.31
Julian Nagele, Christian Sternagel, Thomas Sternagel
Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 72, 2017.

CoCo 2017 Participant: ConCon 1.5
Thomas Sternagel, Christian Sternagel, Aart Middeldorp
Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 75, 2017.

Infinite Runs in Abstract Completion
Nao Hirokawa, Aart Middeldorp, Sarah Winkler, and Christian Sternagel
Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Leibniz International Proceedings in Informatics 84, pp. 19:1 – 19:16, 2017.

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
Proceedings of the 14th International Symposium on Frontiers of Combining Systems, LNCS 10483, pp. 3-21, 2017.

Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
Christian Sternagel, Thomas Sternagel
Proceedings of the 26th International Confluence on Automated Deduction, LNCS 10395, pp. 413-431, 2017.

HOLCF-Prelude
Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel
The Archive of Formal Proofs,  2017.

Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs
Thomas Sternagel and Christian Sternagel
Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 60 – 64, 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, and Christian Sternagel
Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 55 – 59, 2016.

CoCo 2016 Participant: ConCon
Thomas Sternagel and Aart Middeldorp
Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 81, 2016.

CoCo 2016 Participant: CeTA 2.28
Julian Nagele, Christian Sternagel, and Thomas Sternagel
Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 78, 2016.

TTT2 @ TermComp'2016
Christian Sternagel
Proceedings of the 15th International Workshop on Termination (WST 2016),   pp. 23:1, 2016.

The Generalized Subterm Criterion in TTT2
Christian Sternagel
Proceedings of the 15th International Workshop on Termination (WST 2016),   pp. 11:1 – 11:5, 2016.

A Characterization of Quasi-Decreasingness
Thomas Sternagel and Christian Sternagel
Proceedings of the 15th International Workshop on Termination (WST 2016),   pp. 12:1 – 12:5, 2016.

AC Dependency Pairs Revisited
Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari
Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Leibniz International Proceedings in Informatics 62, pp. 8:1 – 8:16, 2016.

Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
Christian Sternagel and Thomas Sternagel
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Leibniz International Proceedings in Informatics 52, pp. 29:1-29:16, 2016.

The Z Property
Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom, and Christian Sternagel
The Archive of Formal Proofs,  2016.

Deriving Comparators and Show Functions in Isabelle/HOL
Christian Sternagel and René Thiemann
Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science 9236, pp. 421 – 437, 2015.

CoCo Participant: CeTA 2.21
Julian Nagele, Christian Sternagel, Thomas Sternagel, René Thiemann, Sarah Winkler, and Harald Zankl
Proceedings of the 4th International Workshop on Confluence (IWC 2015),   pp. 41, 2015.

Level-Confluence of 3-CTRSs in Isabelle/HOL
Christian Sternagel and Thomas Sternagel
Proceedings of the 4th International Workshop on Confluence (IWC 2015),   pp. 28 – 32, 2015.

Certification of Complexity Proofs using CeTA
Martin Avanzini, Christian Sternagel, and René Thiemann
Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Leibniz International Proceedings in Informatics 36, pp. 23 – 39, 2015.

Deriving class instances for datatypes
Christian Sternagel and René Thiemann
Archive of Formal Proofs 2015.