Automation of Rewriting Infrastructure (ARI)

Writing reliable software is a challenging task. Software bugs may result in programs that do not halt or produce different outcomes when this is not desired. In an abstract setting these properties are known as (non-)termination and (non-)confluence. Research teams worldwide are developing software tools that aim to prove or disprove properties like confluence and termination without user interaction. These software tools compete against each other in annual competitions that are organized by the research community. This Austria-Japan joint project is concerned with the development of infrastructure to support the communities involved in confluence and termination research. This includes tool authors and competition organizers. In these communities programs are typically presented as rewrite systems, a simple but powerful abstraction. The project has three main objectives. First of all, we will develop a collection of robust software components for evaluating confluence, termination and complexity tools. The resulting infrastructure will considerably ease the effort to run competitions like the Confluence Competition (CoCo) and the Termination and Complexity Competition (termCOMP). It will also ease access to the tools participating in these competitions and the benchmark problems that these tools are given as input. Since the properties considered in CoCo and termCOMP are undecidable in general and because tools participating in these competitions are highly complex programs, software bugs are common and as a result conflicting answers are produced in competitions. In order to determine which answer can be trusted, human inspection is often infeasible. Consequently, techniques implemented in tools are formalized in a proof assistant such that answers produced by tools can be validated. Since formalization is a challenging and time-consuming task, for many techniques this is not yet achieved. This is particularly true for the newer competition categories in CoCo. A second objective of the project is to formalize techniques that are used in tools that participate in these categories, such that their output can be validated. The third and final objective is to develop new techniques for the analysis of rewrite systems in which rules are equipped with logical constraints which are checked by powerful SMT solvers. These systems are increasingly used in program verification. Besides techniques for confluence, also induction proving techniques are on the agenda. The expected outcome of the project is a software infrastructure that will be adopted by CoCo and termCOMP and that we anticipate to be useful for other competitions in formal methods as well. The formalization efforts will result in more trustworthy tools and we anticipate that some of the current limitations in the use of rewrite systems for program verification will be removed.