Der Informatiker Helmut Veith von der TU Wien erhielt den prestigeträchtigen CAV-Award für computergestützte Verifikation. [...]
Computer machen Fehler, und Fehler sind ärgerlich. Weil kein Mensch ein kompliziertes Programm vollständig analysieren kann, wird diese Aufgabe heute automatisiert: Computerprogramme untersuchen, ob andere Computerprogramme (oder abstrakter ausgedrückt: logische Systembeschreibungen) korrekt sind. Prof. Helmut Veith vom Institut für Informationssysteme der TU Wien forscht seit Jahren mit großem Erfolg auf dem Gebiet Computer Aided Verification (CAV) und Model Checking. Nun erhielt er bei der internationalen CAV-conference gemeinsam mit sieben anderen Forscherinnen und Forschern mit dem CAV-Award, der als international angesehenste Auszeichnung auf diesem Gebiet gilt.
Ein Computerprogramm kann sich in vielen verschiedenen Zuständen befinden. Variablen können unterschiedliche Werte annehmen, und abhängig davon wechselt das Programm in einen neuen Zustand. Überprüft werden soll, ob bestimmte mathematisch formulierte Qualitätsanforderungen in jedem möglichen Zustand und jeder möglichen Programmausführung erfüllt werden. Solche Regeln können beispielsweise darin bestehen, dass das Programm niemals in einer unendlichen Schleife gefangen sein soll, aus der man nicht mehr herauskommt, oder dass bestimmte Werte der Variablen, die das Programm zum Absturz bringen würden, niemals angenommen werden dürfen.
Das System, das man untersuchen möchte, kann man sich wie ein riesiges Netz vorstellen. Jeder Knotenpunkt steht für einen bestimmten Zustand des Programms, und von jedem möglichen Zustand kann man eine bestimmte Anzahl weiterer Zustände erreichen. „Die einfachste Verifikationsmethode wäre es, die Zustände nacheinander zu durchlaufen und zu analysieren, ob es irgendwo zu Fehlern kommt“, erklärt Helmut Veith. „Doch meistens ist die Anzahl der möglichen Zustände so groß, dass das völlig unmöglich ist.“ Mit dem verfügbaren Speicherplatz wächst die Anzahl der möglichen Zustände exponentiell an, daher können solche naiven Testverfahren nur Programme mit sehr kleinem Speicher analysieren. Man muss sich für die Praxis kluge Vereinfachungsstrategien überlegen.
ABSTRAHIEREN UND VERFEINERN
Gemeinsam mit einigen Kollegen entwickelte Helmut Veith vor etwa 15 Jahren das sogenannte „Counterexample-Guieded Abstraction Refinement“ (CEGAR). Dabei wird das Computerprogramm, das untersucht werden soll, zunächst abstrahiert und vereinfacht, und dort wo es nötig ist, wird diese Abstraktion dann Schritt für Schritt verfeinert. „Wenn dann ein Zustand entdeckt wird, der gegen die Qualitätsanforderungen verstößt, muss man zunächst überprüfen, ob es sich tatsächlich um einen Fehler des Programms handelt, oder ob es bloß ein Artefakt aufgrund der Abstraktion ist“, erklärt Helmut Veith. Ein echter Fehler wird gemeldet, ist bloß die Abstraktion am vermeintlichen Problem schuld, wird die Darstellung des Systems verfeinert und die Analyse geht weiter.
Model Checking spielt heute in der Industrie eine wichtige Rolle – sowohl im Bereich der Software als auch der Hardware-Erzeugung. Die CEGAR-Methode gilt als wichtiger Schritt, der die praktische Anwendung von automatisiertem Model Checking in der Industrie erst möglich gemacht hat.
Neben Helmut Veith wurden noch sieben weitere WissenschaftlerInnen mit dem CAV-Award ausgezeichnet – der Turing-Preisträger Edmund Clarke (Carnegie Mellon University), Orna Grumberg (Technion), Ronald H. Hardin, Somesh Jha (University of Wisconsin), Yuan Lu (Atrenta), Robert P. Kurshan (Bell Laboratories) und Zvi Harel (Technion). Übergeben wurden die Preise am 22. Juli.
Helmut Veith studierte an der TU Wien, wo er 1998 auch promovierte (Sub auspiciis praesidentis). Danach ging er an die Carnegie Mellon University in Pittsburgh (USA) und wechselte dann nach Deutschland – zunächst an die TU München, dann an die TU Darmstadt. Seit 2005 ist er Adjunct Full Professor an der Carnegie Mellon University (Pittsburgh, USA), und seit 2009 ist er Professor an der TU Wien. (pi)
Be the first to comment