cl-banner

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

Nach oben scrollen