ERC-Grant für Maria Christakis: Wer kontrolliert die Kontrollore?

Maria Christakis Prof. Maria Christakis entwickelt Software, mit der man man andere Software auf Fehler Überprüfen kann. Dafür erhält sie nun einen hochdotierten ERC-Grant. Jeden Tag sind wir darauf angewiesen, dass Computersoftware korrekt funktioniert. Nicht nur wenn wir Laptops oder Handys benutzen - auch wenn wir in ein Flugzeug steigen, Geld Überweisen oder uns einfach nur auf die Stromversorgung verlassen, sind wir von komplizierter Software abhängig. Die Suche nach Fehlern in dieser Software ist längst automatisiert: Es gibt Computerprogramme, die andere Computerprogramme auf Fehler Überprüfen. Aber wer kontrolliert nun die Software-Kontrollprogramme? Mit dieser höchst diffizilen Frage beschäftigt sich Maria Christakis vom Institut für Information Systems Engineering der TU Wien. Sie wurde nun vom European Research Council (ERC) mit einem ERC Starting-Grant ausgezeichnet - einer der prestigeträchtigsten und höchstdotierten Förderungen der europäischen Forschungslandschaft. Programme, die Programme kontrollieren. In besonders kritischen Bereichen - etwa bei der Steuerung eines Flugzeugs oder eines Kernkraftwerks - möchte man sich nicht damit begnügen, dass die Software bei bisherigen Tests keine Fehler gemacht hat. Man möchte einen Beweis dafür, dass die Software fehlerfrei ist und sich in jeder denkbaren Situation richtig verhält. Dafür verwendet man heute Programm-Analysetools, die auf Basis formaler Logik Computercode untersuchen. In bestimmten Fällen kann man dann mit mathematischer Präzision beweisen, dass ein bestimmter Code tatsächlich absolut fehlerfrei ist. Doch wer analysiert diese Analysetools selbst?