incQuBE

| Beteiligte Mitarbeiter | Beschreibung | Publikationen |

Zusammen mit der STAR-Lab Gruppe der Universität Genua, Italien wurde incQuBE entwickelt. Hierbei wurde der such-basierte QBF Solver QuBE7 um inkrementelles Hinzufügen und Lösen von QBF Problemen sowie die Unterstützung von Assumptions erweitert. Weiterhin werden sog. don't touch Literale eingeführt, so dass im inkrementellen Kontext partielles Präprozessieren der Formel möglich ist, ohne dass bestimmte Variablen eliminiert werden. Dieses Feature wird zum Beispiel beim inkrementellen Bounded Model Checking unvollständiger Schaltkreise verwendet, um die Größe der Transitionsrelation möglichst klein zu halten.