It is important that software works well – especially when safety critical systems are involved, such as medical devices, cars or spacecrafts. Theoretical computer scientists want to check the correctness of software using specification languages derived from logic. Alexandra Silva, PhD student at the Centrum Wiskunde & Informatica (CWI) in Amsterdam, designed a universal framework, Kleene coalgebra, with which such specification languages can be generated automatically. Silva defended her PhD thesis ‘Kleene Coalgebra’ on 21 December 2010 at the Radboud University Nijmegen and graduated with honours – ‘cum laude’. In the future, Silva’s research can be used to improve the quality of software, eg, for the design of electronic circuits.
In safety critical systems, software may not contain any errors. Some people might remember that in the 1980s the Therac-25 radiation therapy machine killed several patients due to several software flaws; in 1996 the Ariane 5 rocket exploded due to a software error. In order to prevent such disasters in the future, theoretical computer scientists express complex computer systems in a mathematical model and test it. (The original system is far too complex to test – that’s why they use a model.) Silva included a large class of models in her theoretical framework, for which she is able to generate both specification languages and axiomatisations. She expects that in the following decade these techniques will have serious impact amongst programmers.
Cum laude
A committee of national and international experts was so impressed by the quality and impact of Alexandra Silva’s thesis that it was awarded the predicate Cum Laude. This in computer science highly exceptional award formed an inspiring starting point for the workshop on Kleene Coalgebra that was held the same day. Speakers were Dexter Kozen (Cornell University), Luis Barbosa (University of Minho, Portugal) and Alexandra Silva. Silva was born in Chaves, Portugal in 1984. Her PhD work has been financed by FCT (Fundação para a Ciência e a Tecnologia) in Portugal, under the auspices of IPA (Institute for Programming research and Algorithmics) in the Netherlands. She is now a postdoc research at the Foundations of Software Engineering group (SEN3) at CWI, starting to make tools for her framework.
More information:
- Supervisor: Prof. dr. J.J.M.M. Rutten (CWI and Radboud University), co-supervisor dr. M.M. Bonsangue (Leiden University)
