Binäre Entscheidungsgraphen
Binäre Entscheidungsgraphen (engl. binary decision diagrams, kurz BDDs) sind eine Datenstruktur für boolsche Funktionen, die eine kompakte computerintere Darstellung und eine effiziente Durchführung boolscher Operatoren (wie Konjunktion, Negation, etc.) ermöglichen. Der BDD-basierte Ansatz (kombiniert mit geeigneten Kodierungstechniken) hat sich in mehreren Anwendungen bewährt. Insbesondere für den Einsatz von CAD-Systemen beim Chipentwurf und die Hardware-Verifikation haben sich BDD-Techniken als besonders effizient erwiesen. Das populärste Beispiel zur Demonstration dieser Aussage ist der berühmt gewordene Fehler im Pentium Dividierer, der nachweislich mit einem BDD-basierten Ansatz hätte gefunden werden können.
In der Vorlesung werden die theoretischen Grundlagen von BDDs, aber auch andere Aspekte, wie Implementierungstechniken, Optimierungsstrategien und deren Anwendungsmöglichkeiten vorgestellt. Der Vorlesungsstoff soll in 2 std. Übungen mit theoretischen und praktischen Aufgaben (mit BDD-Paketen wie CUDD und Verifikations-Tools wie SMV oder VIS) vertieft werden.
Voraussetzungen: Vordiplom in Informatik.
Bereich: Der Vorlesungsstoff kann für eine Diplomprüfung (Bereich A oder C) verwendet werden. Nach Absprache kombinierbar mit anderen Vorlesungen (entweder aus dem Bereich ``Formale Methoden'' oder anderen Prüfern).
Sonstiges: Aktuelle Informationen finden Sie unter der WWW-Seite
http://web.informatik.uni-bonn.de/I/VL/BDD