next up previous
Next: NUSMV: Look and Feel Up: Symbolic Model Checking Previous: Symbolic Representation of Kripke

Fields of Application

The use of BDDs (i.e. the implicit representation of the transition system) makes it possible to verify very large systems (larger than 1020 states [12,47,11]). Symbolic model checking has been successful in various fields, allowing the discovery of design bugs that were very difficult to highlight with traditional techniques. Some of the most significant results are given below (an extensive discussion of the applications of symbolic model checking can be found in [27]):

NuSMV <>