Uni-Logo
English       Login
Rechnerarchitektur
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

incQuBE

| Beteiligte Mitarbeiter | Beschreibung | Publikationen |


Beteiligte Mitarbeiter

Lehrstuhl für Rechnerarchitektur
Paolo Marin, PhD Entwickler / Kontakt


Beschreibung

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.



Publikationen
Enrico Giunchiglia, Paolo Marin, Massimo Narizzano
QuBE7.0, System Description
Journal of Satisfiability, 2010, volume 7, number 8, pages 83--88