Information and Communication Technology 2019ICT19-060

Learning to Solve Quantified Boolean Formulas


Principal Investigator:
Projekttitel:
Learning to Solve Quantified Boolean Formulas
Projektpartner:innen:
Stefan Szeider (Vienna University of Technology) (Co-Principal Investigator)
Status:
Laufend (01.05.2020 – 30.04.2023) 36 Monate
Fördersumme:
€ 330.890

 
Kurzzusammenfassung:

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.

 

Wir nutzen Cookies auf unserer Website. Einige von ihnen sind technisch notwendig, während andere uns helfen, diese Website zu verbessern oder zusätzliche Funktionalitäten zur Verfügung zu stellen. Weitere Informationen