mm1

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
mm1

Verification 2

Subject:

Reduced Ordered Binary Decision Diagrams. Verification using ROBDDs.

Litterature:

(**) Henrik Reif Andersen. An Introduction to Binary Decision Diagrams. DTU, Sep. 1997
(*) Randal E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys, 24(3), pp. 293-318, Sep. 1992. Ask Oliver Möller for this..
(**) Randal E. Bryant. Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, 8(C-35), pp. 677-691, 1986. Ask Oliver Möller for this
New material on BDDs and variations can be found in recent proceedings of CAV, TACAS, LICS, ICCAD, DATE and various journals, for instance, Formal Methods in System Design and Transactions on Computers.
(**) Staunstrup, Larsen, ....: Practical Verification of Embedded Systems, IEEE Computer 2000.

Tool:

To construct BDDs we shall use a tool called Iben developed at BRICS@Aalborg by Gerd Behrmann using. You can find information on how to get access to Iben on the TOOLS page constructed and maintained by Oliver Möller.

One of the currently most efficient BDD packages is the CUDD package developed at University of Colorado.

Excercises:

From the Henrik R. Andersen's BDD notes: Exercises 2.1, 3.2(*), 3.3(*), 3.5, 4.2, 4.4(*), 4.5, 4.7, 6.1(*), 6.3(*), 7.1, and 7.3(*).

Use the Iben to solve the exercises marked with (*). Solutions to boldfaced exercises are to be handed in.