ARI   

ARI: Automation of Rewriting Infrastructure


This Austria-Japan joint project is concerned with the development of infrastructure for software tools that aim to automatically (dis)prove confluence, termination and related properties in a variety of rewrite formalisms, in connection with the Confluence Competition (CoCo) and the Termination and Complexity Competition (termCOMP). In this project we combine the expertise from research teams from

to achieve the following three main objectives:
  1. To develop infrastructure to support the confluence and termination communities (including tool authors, competition organizers, and general researchers). Starting from the existing infrastructure for CoCo (including the Confluence Problems Database COPS and the community-serving web front end CoCoWeb), we will develop a collection of robust software tools for evaluating confluence, termination and complexity methods and tools. The resulting infrastructure will considerably ease the effort to run existing and new competitions in rewriting.
  2. To make tools participating in CoCo more reliable by formalizing techniques in the proof assistant Isabelle/HOL such that more (dis)proofs produced by the tools can be certified, in particular for the commutation and infeasibility categories. Since the properties considered in CoCo and termCOMP are undecidable in general and because tools participating in these competitions are highly complex, formalization and subsequent certification is the only way to ensure formal correctness of the answers provided by the tools, which is not only important for resolving YES/NO conflicts.
  3. To develop confluence and induction proving techniques for logically constrained rewrite systems (LCTRSs), a very expressive rewrite formalism in which rules are equipped with logical constraints which are checked by powerful SMT solvers. LCTRSs are increasingly used in program verification.

Members

The project is coordinated by The Innsbruck team consists of

Open Position

A 3 year postdoctoral position is available.

FWF

ARI will be supported by FWF (I 5943-N) from July 1, 2022 until June 30, 2025.

Contact

Aart Middeldorp (aart middeldorp at uibk dot ac dot at)