Minimal structures for program analysis and verification
Verbeterde formulering van formele methodes voor softwareverificatie
De betrouwbaarheid van softwaresystemen is een belangrijk maatschappelijk probleem. Omdat software veelzijdige functionaliteiten moet bieden in talloze contexten, blijft het bedenken, ontwerpen, en valideren van programma's een complexe taak.
Technieken voor (geautomatiseerde) softwareverificatie zijn erg belangrijk. Tegenwoordig wordt algemeen aanvaard dat formele methoden een doorslaggevende rol kunnen spelen richting betrouwbare software. Formele methoden refereren aan een breed scala aan wiskundige technieken waarmee we software en de beoogde eigenschappen daarvan nauwkeurig kunnen beschrijven. Deze technieken berusten op wiskundige grondslagen en bieden sterke garanties voor correctheid.
De praktische toepassing van formele methoden blijft echter nog achter. Er zijn twee belangrijke uitdagingen: (i) een verhoogde leercurve voor ontwikkelaars, en (ii) de bijbehorende analysetechnieken hebben hun eigen implementatiecomplexiteit. Er is zowel praktisch als theoretisch belang bij het rigoureus bestuderen van eenvoudigere of zelfs minimale formuleringen van de wiskundige structuren die ten grondslag liggen aan formele methoden.
Aran Arslanagic onderzocht in zijn proefschrift twee van zulke wiskundige structuren: typetoestanden en sessietypes. Beide specificeren software-eigenschappen die variëren met de loop van tijd (d.w.z. temporele eigenschappen). Arslanagic toont aan dat eenvoudigere formuleringen van deze structuren kunnen leiden tot zowel praktische als theoretische voordelen. Aan de praktische kant zorgen zijn formuleringen voor aanzienlijke verbeteringen in bruikbaarheid en prestatie, en een gestroomlijnde inbedding in reguliere programmeertalen. Aan de theoretische kant stelt hij een precieze relatie vast tussen zijn formuleringen en de originele, die de voordelen van de toepassing van eenvoudigere formuleringen volledig rechtvaardigen.
Alen Arslanagic voerde zijn promotieonderzoek uit bij het Bernoulli Instituut voor Wiskunde, Informatica en Kunstmatige Intelligentie, bij de groep Fundamentele Informatica. Hij zet zijn loopbaan voort als Research Engineer bij Epic Games, Inc.