1. Einleitung
2. Grundlagen
2.1 Aussagen und Prädikate - 2.2 Mengen, Relationen und Funktionen - 2.3 Graphen - 2.4 Algorithmen und Datenstrukturen - 2.5 Komplexität von Algorithmen - 2.6 Hashverfahren - 2.7 Endliche Automaten und Finite-State-Maschinen - 2.8 Referenzen

Teil I: Datenstrukturen für Schaltfunktionen
3. Boolesche Funktionen
3.1 Boolesche Algebra - 3.2 Boolesche Formeln und Funktionen - 3.3 Schaltfunktionen - 3.3.1 Schaltfunktionen mit höchstens zwei Variablen - 3.3.2 Unterfunktionen und Shannon-Entwicklung - 3.3.3 Visuelle Repräsentation - 3.3.4 Monotone Schaltfunktionen - 3.3.5 Symmetrische Funktionen - 3.3.6 Threshold-Funktionen - 3.3.7 Partielle Schaltfunktionen - 3.4 Referenzen
4. Klassische Darstellungen
4.1 Wahrheitstabellen - 4.2 Zweistufige Normalformen - 4.3 Schaltkreise und Formeln - 4.3.1 Schaltkreise - 4.3.2 - Formeln - 4.4 Binäre Entscheidungsbäume und -graphen - 4.4.1 Binäre Entscheidungsbäume - 4.4.2 Branching-Programme - 4.4.3 Read-once-Entscheidungsgraphen - 4.4.4 Komplexität grundlegender Operationen - 4.5 Referenzen
5. Anforderungen an Datenstrukturen für die formale Schaltkreisverifikation
5.1 Schaltkreisverifikation - 5.2 Formale Verifikation kombinatorischer Schaltkreise - 5.3 Verifikation sequentieller Schaltkreise - 5.4 Referenzen

Teil II: OBDDs: Eine effiziente Datenstruktur
6. OBDDs - Geordnete binäre Entscheidungsgraphen
6.1 Bezeichnungen und Beispiele - 6.2 Reduzierte OBDDs: Eine kanonische Darstellung für Schaltfunktionen - 6.3 Der Reduktionsalgorithmus - 6.4 Grundlegende Konstruktionen - 6.5 Ausführung binärer Operationen und Äquivalenztest - 6.6 Referenzen
7. Effiziente Implementierung von OBDDs
7.1 Schlüsselkonzepte - 7.1.1 Shared OBDDs - 7.1.2 Eindeutigkeitstabelle und strenge Kanonizität - 7.1.3 ITE-Algorithmus und Computed-Tabelle - 7.1.4 Komplementierte Kanten - 7.1.5 Standardtripel - 7.1.6 Speicherverwaltung - 7.2 Einige bekannte OBDD-Pakete - 7.2.1 Das OBDD-Paket von Brace, Rudell und Bryant - 7.2.2 Das OBDD-Paket von Long - 7.2.3 Das CUDD-Paket: Colorado University Decision Diagrams - 7.3 Referenzen
8. Einfluß der Variablenordnung auf die Komplexität von OBDDs
8.1 Zusammenhang zwischen Variablenordnung und OBDD-Größe - 8.2 Exponentielle untere Schranken - 8.3 OBDDs mit verschiedenen Variablenordnungen - 8.4 Komplexität der Minimierung - 8.5 Referenzen
9. Optimierung der Variablenordnung
9.1 Heuristiken für gute Variablenordnungen - 9.1.1 Die Fan-in-Heuristik - 9.1.2 Die Gewichts-Heuristik - 9.2 Dynamisches Umordnen - 9.2.1 Der Variablenswap - 9.2.2 Exakte Minimierung - 9.2.3 Fenster-Permutationen - 9.2.4 Der Sifting-Algorithmus - 9.2.5 Block-Sifting und symmetrisches Sifting - 9.3 Quantitative Aussagen - 9.4 Ausblick - 9.5 Referenzen

Teil III: Anwendungen und Erweiterungen
10. Analyse sequentieller Systeme
10.1 Formale Verifikation - 10.2 Grundlegende Operatoren - 10.2.1 Verallgemeinerte Cofaktoren - 10.2.2 Der Constrain-Operator - 10.2.3 Quantifizierung - 10.2.4 Der Restrict-Operator - 10.3 Erreichbarkeitsanalyse - 10.4 Effiziente Bildberechnung - 10.4.1 Input-Splitting - 10.4.2 Output-Splitting - 10.4.3 Die Transitionsrelation - 10.4.4 Partitionierung der Übergangsrelation - 10.5 Referenzen
11. Symbolisches Model Checking
11.1 Computation Tree Logic - 11.2 CTL-Model Checking - 11.3 Implementierungen - 11.3.1 Das SMV-System - 11.3.2 Das VIS-System - 11.4 Referenzen
12. Varianten und Erweiterungen von OBDDs
12.1 Lockerung der Ordnungsrestriktion - 12.2 Alternative Dekompositionstypen - 12.3 Zero-suppressed BDDs - 12.4 Mehrwertige Funktionen - 12.4.1 Zusätzliche Senken - 12.4.2 Kantenbewertungen - 12.4.3 Momentbasierte Zerlegungen - 12.5 Referenzen
13. Transformationstechniken zur Optimierung
13.1 Transformierte OBDDs - 13.2 Typbasierte Transformationen - 13.2.1 Definition - 13.2.2 Schaltkreisverifikation - 13.3 Lineare Transformationen - 13.3.1 Definition - 13.3.2 Effiziente Implementierung - 13.3.3 Lineares Sifting - 13.4 Codierungstransformationen - 13.5 Referenzen
Literaturverzeichnis
Index