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

P27502

  Contact

christian.sternagel@uibk.ac.at

Publications
  • 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
    The Archive of Formal Proofs,  2018.
  • A verified LLL algorithm
    Ralph Bottesch, Jose Divasón, Max Haslbeck, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
    Archive of Formal Proofs 2018.
  • First-Order Terms
    Christian Sternagel, René Thiemann
    The 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
    The Archive of Formal Proofs, 2015.
Nach oben scrollen