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
project end: January 2018

Members

Christian Sternagel
Thomas Sternagel

FWF project number

P27502

Contact

christian.sternagel@uibk.ac.at

Publications

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

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

Infinite Runs in Abstract Completion
Nao Hirokawa, Aart Middeldorp, Sarah Winkler, Christian Sternagel
2nd International Conference on Formal Structures for Computation and Deduction, 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.

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.

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.

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
The Archive of Formal Proofs, 2015.