Coding projects

Wanda

Although writing code was not the core of my PhD research, syntactic termination methods are usually best demonstrated with a tool that implements them. To this end, I developed WANDA, a termination tool which implements the core of my PhD thesis (as well as some techniques I did not contribute to beyond translating them to WANDA's internal format).

WANDA has been developed for participation in the annual termination competition. Apart from the competition's xml-format, a number of other formats are accepted, as explained in the README.txt file in the downloads.

WANDA can be downloaded from WANDA's page at sourceforge or WANDA's page on Github, and is documented in a conference paper at FSCD 2020.

Underlying theory: WANDA v2.0 (the version available from sourceforge) is primarily based on my PhD thesis. Here it is described how WANDA obtains her results. To some extent, the thesis might be seen as WANDA's (extended) documentation.

WANDA is minimally maintained: no new results have been implemented since 2013. There have only been some minor updates, for instance to improve support for non-pattern input, and to provide formal output for use in certification tools,

Ctrl

One of the targets of the constrained rewriting and SMT project was the development of a tool for rewriting and analysis of constrained term rewriting systems. This tool, Ctrl, is available at http://cl-informatik.uibk.ac.at/software/ctrl/, and is documented in a conference paper at LPAR 2015.

I no longer maintain Ctrl. As the code is open-source, please feel free to use it to make your own spin-off. The main program and name are in principle the property of the Computer Science Logic group in Innsbruck.

Cora

Cora – a COnstrained Rewriting Analyser – is currently still in development. This is a tool meant for various kinds of analysis of first- and higher-order term rewriting, with and without logical constraints. Hence, it could eventually evolve to combine the functionalities of Wanda and Ctrl. Most importantly, though, it is meant as a foundation for student projects in rewriting.

The code is available at Cora's github page, but is not documented (although the formalism is described in the documentation/ directory of the repository). Feel free to use any of the code, but please beware that the documentation may not be up-to-date and the code is constantly changing.