Constrained Rewriting and SMT: Emerging Trends in Rewriting

Term rewriting is an abstract model of computation and the underlying theoretical foundation of declarative programming. Many properties for term rewriting have been studied intensively over the last decades and since a few years there also is an effort to build powerful tools to establish properties for term rewriting systems automatically. This joint project focuses the power of the University of Innsbruck/Technical University of Vienna with four research groups in Japan (Hokkaido University, Japan Advanced Institute of Science and Technology, Nagoya University, University of Yamanashi) and deals with the following five tasks: 1. Constrained Rewriting 2. SMT (Satisfiability Modulo Theories) 3. Completion 4. Complexity 5. Certification The overall aim is to advance applicability of rewriting techniques in verification by focusing on constrained rewriting, a paradigm that suits program analysis better than unconstrained rewriting. Constrained rewriting is a well-studied area but different notions of constrained rewriting exist and only few attempts for automation have been undertaken. Hence a thorough comparison of these approaches is non-trivial. In this project we want to make these approaches comparable, e.g., by a suitable competition of dedicated tools. Nowadays many rewriting tools use so-called SMT solvers as external software to solve (extended) boolean constraints. The second aim of the project is to make (existing) rewriting tools more powerful by extending the underlying SMT solvers with direct support for constrained rewriting. SMT solvers are also essential for some variants and extensions of (Knuth- Bendix) completion which are studied in task 3. The aim of task 4 is to establish upper bounds on the complexity of programs automatically; also here the achievements of tasks 1 and 2 are essential for success. Finally, task 5 addresses to establish soundness of the aforementioned approaches mechanically, i.e., tool (output) is verified automatically with the help of a theorem prover.

The overall aim of the joint project between two universities in Austria and four universities in Japan was to advance the state of the art in constrained rewriting and in the applicability of SMT solvers in rewriting. Rewriting is an abstract model of computation in which sets of directed equations are used to rewrite expressions, for example to simplify them. Such systems of rewrite rules can express arbitrary computer programs. Thanks to the simple theoretical foundation, studying rewrite systems is an attractive stepping stone for developing techniques for analyzing real-life programs. Constrained rewriting is an important variant of rewriting in which the rewrite rules are equipped with constraints that allow to specify their applicability. This makes them better suited for program analysis. An important contribution of this project is the development of a rich framework for rewriting with logical constraints. A software tool, based on powerful SMT solvers, has been developed to support this framework. The framework and supporting tool have been applied to program verification: A large segment of the C programming language has been translated into the framework such that certain verification tasks can be performed automatically. Another important contribution is the development of a notion of complexity for conditional rewriting. Complexity measures the amount of resources needed for computation. Our new complexity notion for conditional rewriting is realistic in the sense that it measures not only successful computations but also partial computations that result in a failed rule. Experiments with the rewrite engine Maude, which is based on conditional rewriting, show the practical importance. Several techniques have been proposed to- wards automatic tool support for establishing tight upper bounds on the complexity of conditional rewrite systems. The final contribution that we mention here is the research on AC-KBO, a termination method for rewrite systems in the presence of associativity and commutativity axioms. We corrected earlier results published in the literature. Experimental results for termination analysis and completion (where the aim is to transform a given axiom system into a rewrite-based presentation) clearly show the benefit of the new method.