Schon mehrfach wurde Laura Kovacs mit hochdotierten ERC-Grants ausgezeichnet. Nun wird sie mit einem "ERC Proof of Concept-Grant" bisherige Erkenntnisse für die Softwareindustrie leichter nutzbar machen.

Am Vortag hatte noch alles funktioniert, doch am 19. Juli 2024 herrschte plötzlich Chaos: Millionen Computer auf der ganzen Welt fielen aus, darunter auch wichtige Systeme von Krankenhäusern, Banken oder Flughäfen. Als "Crowdstrike-Computerausfall" ging dieser Ausfall in die Geschichte ein. Schuld war ein Software-Update, das einen heimtückischen Logik-Fehler enthielt.

Solche Katastrophen sollen sich in Zukunft verhindern lassen - und zwar mit Hilfe neuer Logik-Methoden, die Prof. Laura Kovacs mit ihrem Team am Institut für Logic and Computation der TU Wien in ihrem bisherigen ERC-Projekt entwickelt hat. Nun bekommt sie einen "Proof of Concept-Grant" des European Research Council (ERC), mit dem nun LEARN entwickelt werden soll - eine Schnittstelle, mit der die bereits erarbeiteten logischen Werkzeuge leichter nutzbar gemacht und in der Softwareindustrie eingesetzt werden sollen.

Grant Nummer vier

ERC-Grants sind die höchstdotierten Förderungen der europäischen Forschungslandschaft. Einen solchen Grant einzuwerben, gilt als große Auszeichnung für exzellente wissenschaftliche Arbeit. Laura Kovacs allerdings hat nicht nur einen, sondern nun insgesamt gleich vier ERC-Grants erhalten: Auf einen ERC Starting Grant 2014 folgte ein Proof of Concept-Grant, und auf ihren ERC Consolidator Grant 2020 folgt nun ein weiterer Proof of Concept Grant.

Die Proof of Concept Grants sind dafür gedacht, die wissenschaftlichen Ergebnisse eines bereits erfolgreich abgeschlossenen ERC Grants in die Praxis umzusetzen, etwa indem man ein kommerziell vermarktbares Produkt entwickelt.

Garantiert fehlerfrei

Software ist längst so komplex geworden, dass einzelne Menschen keinen vollständigen Überblick mehr bewahren können. Solche Fehler wie der des Crowdstrike-Updates sind somit auch durch sorgfältige Wartung nicht zu vermeiden. Man kann das Fehlersuchen aber automatisieren: Laura Kovacs arbeitet an logik-basierten Methoden, die bestehende Software analysieren und absolute Fehlerfreiheit garantieren können.

Das Rechnen mit Zahlen wird schon lange von Maschinen viel effizienter erledigt als von Menschen. Auch symbolische Berechnungen, etwa das Umformen und Lösen von Gleichungen, sind für Computer heute kein Problem mehr. Eine neuere Entwicklung ist, dass Maschinen heute auch selbstständig Beweise finden können: Folgt eine bestimmte Aussage logisch zwingend aus bestimmten anderen Aussagen? Kann man zeigen, dass eine bestimmte Aussage (oder eine Liste von Aussagen) immer wahr ist, oder gibt es ein Gegenbeispiel, an das bloß noch niemand gedacht hat?

Solche Logik-Methoden kann man nicht nur auf mathematische Aussagen anwenden, sondern auch auf Computerprogramme: Ist die Software fehlerfrei? Welche Eigenschaften der Software können mit mathematischer Sicherheit garantiert werden? Lässt sich beweisen, dass die Software unter allen logisch möglichen Bedingungen die korrekte Antwort liefert?

Software-Tools dieser Art wurden im Team von Laura Kovacs bereits entwickelt. Nun soll im Rahmen des Proof-of-Concept-Projekts ein Interface namens LEARN entstehen, das diese Methoden auf einfache und leicht zu lernende Weise zugänglich macht.

Großes Interesse aus der Software-Industrie

"LEARN wird auf diese Weise gewaltige Kosten einsparen können, die für das Korrigieren fehlerhafter Software-Updates immer wieder anfallen", sagt Laura Kovacs. "LEARN konzentriert sich auf zwei Dinge: Erstens können Leute, die in der Softwareentwicklung tätig sind, damit logische Modellierung lernen. Sogar für alle jene, die in dem Bereich noch wenig Erfahrung haben, soll LEARN durch ein einfaches, interaktives Inferface leicht nutzbar sein. Zweitens entwickelt LEARN selbstständig Beweis-Strategien, um die Sicherheit des Systems garantieren zu können."

Der Proof of Concept Grant ist mit €150.000 dotiert, über einen Projektzeitraum von 1,5 Jahren. Das Produkt wird in industriellen Umgebungen eingesetzt werden - weltbekannte Firmen wie Amazon, Certora und Microsoft haben bereits als "early adopter" zugesagt. Außerdem soll LEARN auch in der Lehre eine sichtige Rolle spielen: Hunderte Studierende werden an der TU Wien die Möglichkeit haben, mit Hilfe des Tools ihre Logik und Softwareanalyse-Fähigkeiten zu verbessern.

Rückfragehinweis
Prof. Laura Kovacs
Institut für Logic and Computation
Technische Universität Wien
+43 1 58801 18430
laura.kovacs@tuwien.ac.at

Aussender:
Dr. Florian Aigner
PR und Marketing
Technische Universität Wien
Resselgasse 3, 1040 Wien
+43 1 58801 41027
florian.aigner@tuwien.ac.at