Turing-Preis für Entwickler der formalen Verifikation
Amerikanische und französische Wissenschaftler erhielten den als "Nobelpreis der Informatiker" angesehenen Turing-Preis 2007.
Der von der Association for Computing Machinery (ACM) alljährlich verliehene Turing-Preis in Höhe von insgesamt 250.000 US-Dollar – mitgesponsert von Intel und Google – ging an die Entwickler der formalen Verifikation: Edmund M. Clarke, Allen Emerson und Joseph Sifakis. Vor rund 25 Jahren hatten Clark und Emerson an der Harvard University und unabhängig davon Joseph Sifakis an der Université de Grenoble Verfahren entwickelt, um die korrekte Funktion eines komplexen Systems anhand von mathematischen Methoden nachzuweisen (Äquivalenz-Checker, Modell-Checker). Diese formale Verifikation ist in vielen Fällen der Simulation überlegen; ohne solch mathematisches Rüstzeug wären komplexe Gebilde wie Prozessoren, Busprotokolle wie PCI etc. heutzutage kaum mehr machbar.
Sifakis leitet inzwischen die Firma Verimag, Clarke ist Professor an der Carnegie Mellon School of Computer Science und Emerson am Department of Computer Science der University of Texas, wo etwa zeitgleich mit der Verkündung des Turing-Preises der mit 320 TFlop/s Linpack-Rechenleistung schnellste zivile Supercomputer der Welt, der Ranger, seinen Vollbetrieb aufnahm. Und schnelle Rechner braucht man bei der formalen Verifikation, wo oft tausend und mehr Zustandsvariable zu berücksichtigen sind. (as)
