NIA | Informal Seminar Series

Informal Seminar by Radu Siminiceanu

Date: January 18, 2006
Time: 12:00pm
Location: NIA, Rm 137

The BDD Revolution
Radu Siminiceanu, NIA
Binary Decision Diagrams (BDD) are one of the biggest breakthroughs in Computer Aided Design and Verification in recent years. BDDs are a canonical and efficient way to represent and manipulate Boolean functions and have been successfully used in numerous CAD applications, by allowing the full representation of very large state spaces (often of 10²⁰ states and beyond). Although the basic idea of BDDs has been around for nearly 50 years, it was a paper by R.Bryant in 1986 that described a canonical BDD representation and efficient implementation algorithms. So important was the impact of this paper in automated verification, that BDDs have now been "borrowed" by dozens other related fields. At the same time, Bryant's paper has become, in record time, the most cited paper in all Computer Science.

This talk is dedicated to a low-level introduction to BDD representations and applications. The second part of this seminar will introduce SMART, a software tool that we developed in the recent years for the exhaustive verification of system properties (known as symbolic model checking, an alternative to testing and simulation). A real case study of industrial size will demonstrate the capabilities of this technique.

If you are using large data structures and need better methods for their compact representation and efficient manipulation (and have not heard of BDDs yet) this talk is for you!