Specificatie en Verificatie van Imperatieve Programma's.

Het schrijven van betrouwbare en correcte programma's is moeilijk. Programma verificatie is een software ontwikkelingstechniek die programmeurs in staat stelt om de afwezigheid van fouten in hun programma's te garanderen. Hoewel verificatie grote vooruitgang heeft geboekt in het voorbije decennium, is de techniek nog steeds geen volwaardig alternatief voor testing. De lange-termijn, ambitieuze doelstelling van mijn onderzoek is om formele verificatie voor imperatieve programma's te ontwikkelen tot een volwaardige software ontwikkelingsdiscipline. In dit onderzoeksproject ga ik me focussen op vier belangrijke uitdagingen voor verificatie: (1) het frame probleem, (2) redeneren over meerdradige programma's, (3) het gebruik van closures en (4) het verbeteren van de bruikbaarheid van verificatietools door betere feedback naar programmeurs en nauwere integratie met andere ontwikkelingstools.

Trefwoorden:Imperative programs

Disciplines:Toegepaste wiskunde, Computerarchitectuur en -netwerken, Distributed computing, Informatiewetenschappen, Informatiesystemen, Programmeertalen, Scientific computing, Theoretische informatica, Visual computing, Andere informatie- en computerwetenschappen