Man gibt gewünschte Eigenschaften eines Programms oder einer elektronischen Schaltung, etwa eines Computerchips, in eines dieser Software-Werkzeuge ein und lässt es rechnen. Geht alles glatt, spuckt es kurze Zeit später eine Lösung aus: einen fehlerfreien Algorithmus, der den gegebenen Spezifikationen entspricht.

Synthesetools heißen solche Hilfsprogramme. Martina Seidl vom Institut für Formale Methoden und Verifikation der Johannes-Kepler-Universität (JKU) Linz hat, gemeinsam mit ihrem Kollegen Robert Könighofer von der TU Graz, an einem neuen Ansatz im Bereich dieser Anwendungen gearbeitet. Mit Erfolg: Den entsprechenden Wettbewerb, die "Reactive Synthesis Competition" bei den Olympischen Spielen der Logik, die heuer im Rahmen des Wiener Summer of Logic stattgefunden haben, haben sie gewonnen.

Das Besondere daran: Das Synthesetool von Seidl und ihrem Grazer Kollegen, das sie im Rahmen des vom Wissenschaftsfonds FWF geförderten Projekts "RiSE: Rigorous Systems Engineering" entwickelten, verwendet Quantifizierte Boolesche Formeln (QBF), eine elementare logische Sprache, die durch sogenannte Quantoren erweitert wird.

"Man kann es als Spiel erklären", erläutert Seidl ihren Forschungsschwerpunkt. "Durch die Quantoren haben wir zwei Spieler: den universellen Spieler, der die Variablen so zu belegen versucht, dass die Formel falsch wird; und den existenziellen Spieler, der Belegungen finden soll, sodass die Formel wahr wird."

Das Spiel hat bestimmte Regeln, was die Reihenfolge der Spielzüge und Abbruchkriterien betrifft. Die Anzahl der Möglichkeiten, die Variablen zu belegen ist exponentiell, es gibt also so viele Kombinationen, dass es nicht möglich ist, sie alle durchzuprobieren, erklärt Seidl. "Ich beschäftige mich in meiner Forschung damit, wie man diese Probleme trotz des großen Suchraums lösen kann. Es geht um Optimierungstechniken für das Lösen solcher Formeln."

Man könnte beispielsweise auch das bekannte Spiel Tic Tac Toe als QBF kodieren und sagen: "Egal wie der beginnende Spieler A seine Züge wählt, Spieler B kann immer verhindern, dass A gewinnt." Seidl: "Unsere Software könnte, vereinfacht gesagt, berechnen, wie B seine Züge wählen muss, damit A nicht gewinnt." Es wird ein Programm generiert, das der vorgegebenen Eigenschaft - A gewinnt nicht - entspricht. "Das ist jetzt ein sehr einfaches Beispiel, aber es zeigt das Prinzip."

Die 1980 in Klosterneuburg geborene Computerwissenschafterin hat im Rahmen der Logik-Olympiade auch selbst eine Competition organisiert, in der es darum ging, vorgegebene QBF-Probleme möglichst schnell zu lösen. Die Schwierigkeit für Seidl bestand darin, eine objektive Evaluierung sicherzustellen. "Jeder kann Formeln einreichen, die dann von der Community bearbeitet werden. Das führt zu neuen Forschungszielen und letztendlich zu besseren und stabileren Programmen."

Auch ihre Dissertation an der TU Wien schrieb Seidl bereits zu Quantifizierten Booleschen Formeln. Mit der Knowledge-Based Systems Group und der Business Informatics Group dort kooperiert sie bei wissenschaftlichen Projekten bis heute. Woher ihr Interesse an Informatik kommt? "Zum Beispiel von Mittelschullehrern, die sehr offen für neue Technologien waren und es geschafft haben, die richtigen Anreize zu bieten. (Alois Pumhösel, DER STANDARD, 3.9.2014)