VERBS: Verification of Finite State Systems by Bounded Correctness Checking

download of VERBS (verbs1.35.tar)

Running the Program (Tested on a Linux Platform with 128GB Memory)
  • run "tar -xvf verbs1.35.tar" to unpack the file.
  • type "cd verbs" to go to the program directory.
  • run "./verbs examples/mutex01.vvm" to check the program execution.

    Documentations

    Wenhui Zhang.
    verbs: Verification of Finite State Systems based on Bounded Correctness Checking.
    -- An introduction to the verification tool.

    Wenhui Zhang.
    Testing and Experimental Evaluation of QBF-based Bounded Correctness Checking.
    -- An experimental evaluation report, with a comparison with NuSMV 2.5.0 based on a set of test cases (download the test cases).

    References

    Wenhui Zhang.
    SAT-Based Verification of LTL Formulas.
    Lecture Notes in Computer Science 4346 (FMICS/PDMC 2006):277-292. Springer-Verlag. 2007.

    Wenhui Zhang.
    Model Checking with SAT-Based Characterization of ACTL Formulas.
    Lecture Notes in Computer Science 4789(ICFEM 2007):191-211. Springer-Verlag. 2007.

    Wenhui Zhang.
    Bounded Semantics of CTL and SAT-based Verification.
    Lecture Notes in Computer Science 5885 (ICFEM 2009):286-305. Springer-Verlag. 2009.

    Old versions

    Old versions are available by following this link