Het is belangrijk dat software goed werkt, vooral wanneer er veiligheidskritische systemen bij betrokken zijn - zoals medische apparatuur, auto’s of raketten. Theoretisch informatici stellen voor om de correctheid van software controleren met specificatietalen die afgeleid zijn uit de logica. Alexandra Silva, promovenda van het Centrum Wiskunde & Informatica (CWI) in Amsterdam, ontwierp een universeel raamwerk, Kleene coalgebra, waarmee zulke specificatietalen automatisch gegenereerd kunnen worden. Silva verdedigde haar proefschrift 'Kleene Coalgebra' op 21 december 2010 aan de Radboud Universiteit Nijmegen en kreeg daarvoor het predicaat 'cum laude'. In de toekomst kan haar onderzoek gebruikt worden voor het verbeteren van de kwaliteit van software, bijvoorbeeld bij het ontwerp van elektronische circuits.
Software in veiligheidskritische systemen mag geen fouten bevatten. Sommige mensen herinneren zich misschien nog dat in de jaren '80 van de vorige eeuw het Therac-25 bestralingsapparaat de dood van meerdere patiënten veroorzaakte ten gevolge van softwaregebreken – en in 1996 explodeerde de Ariane 5-raket ten gevolge van een fout in de software. Om dit soort rampen in de toekomst te voorkomen, drukken theoretisch informatici computersystemen uit in een wiskundig model en testen dat vervolgens. (Het oorspronkelijke systeem is te complex om te testen; daarom gebruiken ze een model.) Silva voegde een grote klasse modellen aan haar raamwerk toe, waarvoor ze zowel de specificatietalen als axiomatisaties kan genereren. Ze verwacht dat deze technieken onder programmeurs in het komende decennium serieuze impact zullen hebben.
Cum laude
Een commissie van nationale en internationale experts was zo onder de indruk van de kwaliteit en impact van het proefschrift van Alexandra Silva dat zij het predikaat cum laude kreeg. Deze in de informatica zeer uitzonderlijke toekenning vormde een inspirerend uitgangspunt voor de workshop over Kleene Coalgebra die op dezelfde dag werd gehouden. Sprekers waren Dexter Kozen (Cornell University), Luis Barbosa (University of Minho, Portugal) en Alexandra Silva. Silva werd geboren in Chaves, Portugal, in 1984. Haar promotieonderzoek is gefinancierd door FCT (Fundação para a Ciencia een Tecnologia) in Portugal, en is uitgevoerd onder auspiciën van IPA (Institute for Programming research and Algorithmics) in Nederland. Ze is nu postdoc onderzoeker in de Foundations of Software Engineering groep (SEN3) op het CWI, waar ze tools voor haar framework gaat maken.
Meer informatie:
- http://homepages.cwi.nl/~ams/ en http://www.cwi.nl/sen3.
- Promotor: prof. dr. J.J.M.M. Rutten (CWI en Radboud Universiteit), co-promotor dr. M.M. Bonsangue (Universiteit Leiden).
