Modulaire formele verificatie van totale correctheidseigenschappen van meerdradige imperatieve programma's

Voor software-ontwikkelingsprojecten met zeer hoge correctheidsvereisten (bv. in het geval dat het systeem bij foute werking schade zou kunnen berokkenen aan personen of goederen, of dat het systeem met het internet verbonden is en dus bestand moet zijn tegen cyber-aanvallen, of dat het systeem snel moet reageren op gebeurtenissen), kan er in veel gevallen niet voldoende zekerheid verkregen worden van de correctheid met klassieke kwaliteitscontroletechnieken zoals testen en codenazicht. De alternatieve aanpak van formele verificatie, daarentegen, waarbij wiskundige methodes gebruikt worden om wiskundig te formuleren en te bewijzen dat het systeem voldoet aan de bedoelde correctheidseigenschappen, kan een veel grotere zekerheid bieden. In dit project zal ik onderzoek doen naar het verbeteren van de stand van de wetenschap en technologie in dit gebied om het economisch haalbaarder te maken om formele verificatie toe te passen in de praktijk en software-ontwikkelingsteams toe te laten kostenefficiënt producten met hoge zekerheid van correctheid af te leveren. Ik zal mij in het bijzonder richten op de belangrijke maar complexe aspecten van terminatie en productiviteit (liveness) en gelijktijdigheid (concurrency, waarbij het programma slechts een partiële orde specificeert op de uitvoeringsstappen, wat leidt tot een explosie van het aantal mogelijke uitvoeringen).