Formale Beweismethoden
G | 03-IBAP-FBM
In diesem Kurs lernen Studierende verschiedene kompakte
und eindeutige Darstellungen von Booleschen und
Pseudo-Booleschen Funktionen kennen – darunter BDDs
(Binary Decision Diagrams) und KFDDs
(Kronecker Functional Decision Diagrams). Der Fokus liegt
auf der Anwendung von Syntheseoperatoren, der Analyse von
Laufzeitverhalten sowie der Optimierung der Variablenordnung
zur Effizienzsteigerung. Ergänzend werden alternative
Entscheidungsdiagramme für Pseudo-Boolesche Funktionen
behandelt. Die Teilnehmenden arbeiten mit modernen
Solver-Technologien wie SAT und SMT und lernen deren
Funktionsweise und Einsatzmöglichkeiten kennen.
Ziel ist es, formale Beweismethoden in realen
Anwendungsszenarien bewerten und gezielt einsetzen zu
können.
