VERDS

Evaluation of VERDS Version 1.32

• Testing and Evaluation (done on a Linux Platform with 128 GB memory)

Details: This document contains an evaluation consisting of two parts:

Evaluation of the efficiency of the implementation based on boolean diagrams (called boolean diagram model checking) in verds.

• This evaluation of boolean diagram model checking is relative to NuSMV 2.5.0 (BDD based symbolic model checking) with experimental data based on two types of handcrafted boolean programs, and two types of random boolean programs.

Evaluation of the efficiency of the implementation based on bounded semantics (called bounded semantics model checking) in verds.

• This evaluation of bounded semantics model checking is relative to the boolean diagram model checking implemented also in the same tool based on the same sets of boolean programs mentioned above.