Vrije Universiteit Amsterdam
Vrije Universiteit Amsterdam Meer perspectief
7 juni 2010
Methoden ontwikkeld voor automatische analyse programmacorrectheid
Met de toenemende complexiteit van computersystemen is programmaverificatie van centraal belang geworden in de informatica. Daarbij hebben we automatische hulpmiddelen nodig die de verificatie ondersteunen van essentiële aspecten van programmacorrectheid, in het bijzonder terminatie en productiviteit. Joerg Endrullis ontwikkelde methoden voor de automatische analyse van terminatie en productiviteit. Hij promoveerde 1 juni aan de faculteit Exacte Wetenschappen van de VU.
Endrullis bestudeerde twee cruciale aspecten van programmacorrectheid: terminatie en productiviteit. Een programma heet terminerend als de berekening na eindig aantal stappen eindigt. Met andere woorden: de berekening stopt in eindige tijd. Meestal verlangen we van programma's dat ze terminerend zijn. Zelfs niet-terminerende 'control' programma's zoals Windows en Word bestaan voor een groot deel uit terminerende functie-aanroepen; terminatie van deze functies is essentieel omdat 'control' terug moet keren naar de hoofd 'control loop', anders 'hangt' het programma.
Productiviteit daarentegen betreft niet-terminerende processen. Productiviteit belichaamt de intuïtieve notie van onbegrensde voortgang, van werkende programma's die onbeperkt veel gedefinieerde waarden produceren. Bijvoorbeeld de bovengenoemde programma's moeten productief zijn; ze moeten output blijven produceren, dat wil zeggen, ze moeten ontvankelijk blijven voor inputs van de gebruiker. Bovendien is productiviteit belangrijk voor terminerende programma's die werken met specificaties van oneindige structuren zoals oneindige lijsten of bomen. Voor de correctheid van zulke programma's moet gegarandeerd zijn dat elk eindig deel van de oneindige structuur inderdaad kan worden gevalueerd, dat wil zeggen, de specificatie van de structuur moet productief zijn.
Vrije Universiteit Amsterdam