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.

One of the most widely used devices of program verification is the application of equations (for example, in order to replace part of a program by more efficient code that yields the same results). The problem with equations is that you can apply them in both directions: from left to right and from right to left. Therefore, when applying equations we can never be quite sure whether we are actually coming closer to our goal and when to stop. This problem is tackled by term rewriting, where we replace equations by rules that can only be applied from left to right. Two of the most important properties of the resulting term rewrite systems (TRSs for short) are termination and confluence. Termination means that there are no infinite loops: we always arrive at some result to which no rules apply. And confluence states that independent of the order in which we apply rules, we never destroy anything, but are always able to reach all results. A TRS that enjoys both of these properties is especially useful, since a computer can automatically apply its rules in an arbitrary order and will always reach unique results. This is also why we are interested in what is called completion, a process that starts from a set of equations (for example characterizing a program mathematically) and on success delivers a terminating and confluent TRS that satisfies all the original equations. The "Certification Redux" project was concerned with refining what is called the certification approach. This is a general approach for the automated verification of term rewriting related properties, where we employ and develop two kinds of tools: On the one hand, automated provers, that is, programs that can for example check termination or confluence of TRSs automatically and in case of success generate a corresponding proof, a so called certificate. On the other hand, a certifier that is responsible for validating the certificates that were generated by automated provers. Now it would be insufficient to just implement the certifier as standard computer program that checks certificates for correctness: Why should we trust such a program any more than the automated provers? In order to guarantee the highest possible degree of reliability, we instead prove the correctness of the certifier with a proof assistant. As outcome of our project we are now able to automatically prove and certify confluence of TRSs with rules that are guarded by conditions. Moreover, we captured the theory of completion inside a proof assistant and are now able to certify an especially successful but also complex variant of completion: ordered completion. Both results constitute useful tools for program verification.