Formale Verifikation

Startseite
Binary Decision Diagrams (BDDs) ● Theorie der BDDs wurde bereits um 1960 entwickelt. ● BDDs sind eine kanonische Darstellung für boolesche Funktionen. ● Bryant zeigte 1986, dass fast alle logischen Operationen sehr effizient auf BDDs durchgeführt werden können, sofern eine feste Variablenordnung zugrundegelegt wird und gewisse Reduktionsregeln auf die BDDs angewandt werden. ● Durchbruch in der formalen Verifikation.    

Binäre Entscheidungsgraphen wurden durch R. E. Bryant entscheidend weiterentwickelt. Mit dieser Art von Graphen lassen sich boolesche Funktionen in einer sowohl kanonischen als auch kompakten Darstellung speichern und verarbeiten.