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

• Japan Advanced Institute of Science and Technology
• Niigata University
• National Institute of Advanced Industrial Science and Technology
• Nagoya University
• University of Innsbruck

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

• Nao Hirokawa (coordinator Japan)
• Aart Middeldorp (coordinator Austria)

The Innsbruck team consists of

• Gernot Baumgartner
• Dohan Kim
• Aart Middeldorp
• Fabian Mitterwallner
• Jonas Schöpf
• René Thiemann

Meetings

• kickoff meeting, September 5 – 9, 2022, University of Innsbruck
• midterm meeting, August 21 – 22, 2023, Obergurgl
• final meeting, February 20 – 23, 2024, Kira Onsen

FWF

ARI is 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)