-
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 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.