Vrije Universiteit Amsterdam

Terminatie en productiviteit


* Startdatum: 01-06-2010


* Tijd: 13.45


* Locatie: Auditorium


* Titel: Termination and Productivity


* Spreker: J. Endrullis


* Promotor: prof.dr. J.W. Klop


* Onderdeel: Faculteit der Exacte Wetenschappen


* Wetenschapsgebied: Exacte wetenschappen


* Evenementtype: Promotie

Met de toenemende complexiteit van computersystemen is programmaverificatie van centraal belang geworden in de informatica. Om de toenemende complexiteit van software- en hardwaresystemen het hoofd te bieden, hebben we automatische hulpmiddelen nodig die de verificatie ondersteunen van `zekere' aspecten van programmacorrectheid. Joerg Endrullis ontwikkelde methoden voor de automatische analyse van terminatie en productiviteit.

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.

© Copyright Vrije Universiteit Amsterdam