Home | Publications | CV | Software | Links

Synchronization Verification Tool (S-VeT)



    January 11, 2007      S-VeT version 0.1 is available for download


    Version Binary Manual
    0.1 S-VeT_bin.tar.gzManual-0.1


    This work is supported by Semiconductor Technology Academic Research Center (STARC) and Japan Society for the Promotion of Science (JSPS)


    S-VeT is a tool that used to verify synchronization in SpecC descriptions. Implementation of S-VeT is similar to other well-known C verifiers like SLAM, BLAST, and MAGIC. However, in order to cope with non-deterministic behavior of statement execution in SpecC, execution of every statement is described with equality/inequality formulae and solved by using commercial ILP solver.


    S-VeT has been successfully installed on Fedora Core 3, 4 and GCC 3.0-3.4. In order to run S-VeT smoothly, you will need to install the following tools.
    1. SpecC reference compiler version 2.2.0
    2. NuSMV
    3. CVC Lite
    4. ILOG Cplex


    We appreciate for any comment and/or bug reports from you. Also, if you have any question, please feel free to contact me.