Programmeerprojecten

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.

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 regelmatig nieuwe ontwikkelingen op het gebied van hogere orde terminatie implementeer (waarbij ik me concentreer op technieken waar ik zelf aan heb bijgedragen).

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.

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 documentatie van WANDA.

Termherschrijf Bibliotheek

Een makkelijke bibliotheek in C++ die met termherschrijfsystemen kan werken heeft meer nut dan alleen als terminatie tool. Zodoende is deze bibliotheek zo algemeen mogelijk. De code kan gebruikt worden voor complexere toepassingen (zoals WANDA), het programma zelf doet niet veel.