Verification based on Bounded Semantics

Please check the extension of this tool, called verds.
The new features include: an implementation of boolean diagram model checking and QBF-based bounded semantics model checking,
http://lcs.ios.ac.cn/~zwh/verds/
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.
Bounded Semantics of CTL and SAT-based Verification.
Lecture Notes in Computer Science 5885 (ICFEM 2009):286-305. Springer-Verlag. 2009.

download of VERBS (verbs1.25.tar)
Compilation Steps
  • run "tar -xvf verbs1.25.tar" to unpack the file.
  • type "cd verbs" to go to the program directory.
  • update "config.h" for specification of the SAT-solver to be used.
  • type "make" to compile the program.
  • run "./verbs ver/p1uu09ik.ver" to check the program execution.

    download of VERBS (verbs1.27.tar)
    Compilation Steps
  • run "tar -xvf verbs1.27.tar" to unpack the file.
  • type "cd verbs" to go to the program directory.
  • update "config.h" for specification of the SAT-solver to be used (recommended).
  • type "make" to compile the program.
  • run "./verbs ver/rr09vp7.ver" to check the program execution.