Learning to Solve Quantified Boolean Formulas

Die fortschreitende Digitalisierung aller Lebensbereiche stellt unsere Gesellschaft vor immer neue Herausforderungen. Die Sicherheit und Zuverlässigkeit komplexer und ständig im Wandel begriffener Softwaresysteme sind schwer zu überprüfen, und beinahe täglich werden neue Sicherheitslücken bekannt. Bei herkömmlicher Software können diese Schwachstellen nach und nach durch regelmäßige Updates behoben werden. Bei sicherheitskritischen Systemen ist ein derartiges Vorgehen inakzeptabel. Hier müssen von Anfang an die höchsten Standards angewandt werden. Im Idealfall sollte die korrekte Implementierung solcher Systeme in Übereinstimmung mit einer präzise formulierten Spezifikation sichergestellt sein. Hier gibt es zwei Möglichkeiten: 1) Man versucht, ein der Spezifikation entsprechendes System von Hand zu entwerfen und dessen Korrektheit zu beweisen. 2) Man erzeugt rechnergestützt direkt aus der Spezifikation ein System, das beweisbar der Spezifikation entspricht. Das vorliegende Projekt beschäftigt sich mit Methoden, die den zweiten, als "Synthese" bezeichneten Ansatz unterstützen. Konkret werden Verfahren zum Lösen von sogenannten Quantifizierten Bool'schen Formeln (QBFs) untersucht, in denen Spezifikationen von Systemen wie etwa Hardwarecontrollern kompakt formuliert werden können. Aus der Lösung einer QBF kann entweder ein der Spezifikation entsprechendes System abgelesen werden, oder ein Beweis dafür, das kein entsprechendes System existiert.