Download VeriSoft

This package includes a version of VeriSoft for analyzing multi-process C or C++ programs whose processes communicate via a predefined set of types of communication objects. The package also includes simple examples of concurrent C programs and a reference manual.

This version of VeriSoft is for educational use and evaluation purposes only. Please see the VeriSoft [FAQ] or contact the authors (see [Contact us!]) for information concerning the availability of VeriSoft for other platforms (SGI, HP,...), other languages (Java, Tcl,...), and other libraries of communication objects (shared memory, files, timers,...). If there is enough interest for other platforms/languages/objects, we may try to extend the scope of the distribution package accordingly. However, please note that VeriSoft is a research project and prototype, and that support for the free version is limited.
 

Installation Instructions

• Tcl is a scripting language and Tk is a Tcl application that provides a programming environment for creating graphical user interfaces under X windows. Tcl/Tk can be downloaded from http://www.scriptics.com/. Install Tcl/Tk with dynamic loading enabled (the default option). Recommendation: use tcl7.6 and tk4.2 or more recent versions.
• Expect is another Tcl application for automating the control of interactive programs. Expect can be downloaded from http://expect.nist.gov/. Install Expect in combination with Tk in order to generate an executable file named "Expectk". Recommendation: use expect-5.24 or a more recent version.
• gdb is a debugger for programming languages including C and C++. It can be downloaded from http://www.gnu.ai.mit.edu/home.html.

• uncompress verisoft.tar.Z
• tar xvf verisoft.tar

Then, follow the instructions given in the file INSTALL-README in that directory.