Programmeerprojecten

Wanda

Alhoewel het schrijven van code niet de kern van mijn promotie-onderzoek was, is het zeker waar dat (syntactische) terminatiemethoden vaak het best te demonstreren zijn met een implementatie. Daarvoor dient WANDA, een terminatie tool waarin ik de kern van mijn proefschrift heb geimplementeerd (naast ook ontwikkelingen waar ik niet aan heb bijgedragen buiten de vertaling naar het interne formaat van WANDA).

WANDA is gericht op deelname in de jaarlijkse terminatie competitie. Buiten het xml-formaat van de competitie worden een aantal andere formaten geaccepteerd; dit wordt beschreven in de README.txt file in de downloads.

WANDA kan worden gedownload op WANDA's pagina op sourceforge of WANDA's pagina op Github en is gedocumenteerd in een conferentie paper voor FSCD 2020.

Gebruikte resultaten: WANDA v2.0 (de versie die beschikbaar is op sourceforge) is vooral gestoeld op mijn proefschrift. Hierin wordt ook beschreven hoe WANDA aan haar resultaten komt. De connectie gaat zo ver dat, tot op zekere hoogte, het proefschrift gezien kan worden als de (uitgebreide) documentatie van WANDA.

WANDA wordt momenteel minimaal bijgehouden: er zijn sinds 2013 geen nieuwe resultaten geimplementeerd, maar wel kleine aanpassingen gedaan; bijvoorbeeld bredere ondersteuning van non-pattern invoer, en formele uitvoer die andere tools kunnen gebruiken.

Ctrl

Een van de doelen van het constrained rewriting and SMT project was het schrijven van een tool waarmee termherschrijfsystemen met beperkingen kunnen worden herschreven, en geanalyseerd. Dit tool, Ctrl, is beschikbaar op http://cl-informatik.uibk.ac.at/software/ctrl/, en is gedocumenteerd in een conferentie paper voor LPAR 2015.

Ik werk niet meer aan Ctrl. De code is open-source, dus voel je vrij om je eigen spin-off te maken; het hoofdprogramma is in principe de eigendom van de Computer Science Logic groep in Innsbruck.

Cora

Cora – kort voor COnstrained Rewriting Analyser – is nog volop in ontwikkeling. De bedoeling is om uiteindelijk Cora te ontwikkelen tot een brede analysetool voor verschillende soorten analyse van verschillende soorten herschrijfsystemen (eerste of hogere order, met of zonder constraints). Het is dus zeker mogelijk dat het uiteindelijk de functionaliteiten van Wanda en Ctrl zal combineren. De prioriteit is echter vooral dat Cora bedoeld is als een basis voor studentenprojecten in termherschrijven.

De code is beschikbaar op de Github pagina van Cora, maar is niet echt gedocumenteerd (het formalisme wordt uitgelegd in de documentation/ map in de repository, maar deze wordt niet continu up-to-date gehouden met de huidige status van de code, dus kan incorrect zijn). Voel je vrij om de code volledig of deels te gebruiken, maar hou er rekening mee dat ik geen garanties over de kwaliteit kan geven, en dat de code continu aan het veranderen is.