Linking QEPCAD with PVS

SACLIB, QEPCAD, QEPCAD-PVS, SAL

Download QEPCAD-PVS

Download the gzipped tar file from here , and follow the instructions in the README file (also reproduced below).

How to use qepcad through PVS:

Step 1: Make the binaries required for qepcad
-- run "make clean" followed by "make" in this directory
Note: "make" uses the saclib and qepcad files that are in ~tiwari/softwares/something. If you can't access this, then install saclib, followed by qepcad, as said below.
-- if "make" succeeds, then you should see a file "qepcad.so" in this directory.

Step 2: Load qepcad into PVS -- load the file "qepcad.lisp" present in this directory into PVS by calling (load "qepcad.lisp")
Note: Make sure the directory in "qepcad.lisp" is specified correctly.

Step 3: Test on sample examples
-- Change context to the "Examples" subdirectory.
-- Try to run the proofs of some of the theorems in 1.pvs and 2.pvs

Download SACLIB

Download the gzipped tar file from here for SACLIB2.1 (Linux), and follow the following instructions to install SACLIB (don't read any of the README files in the tar-file, they are confusing):

Step 1: Uncompress
-- gunzip ; tar -xvf creates a directory "saclib2.1". Let us say the full pathname is "/base-directory/saclib2.1"

Step 2: Run the following command 

 -- /base-directory/saclib2.1/sysdep/linux/install   /base-directory/saclib2.1

Note: This will take around 4 minutes.

Step 3: Test
-- Check if you have successfully created the library /base-directory/saclib2.1/lib/libsaclib.a

Download QEPCAD

Download the gzipped tar file from here for QEPCAD (Linux), and follow the following instructions to install QEPCAD (don't read any of the README files in the tar-file, they are confusing):

Step 1: Uncompress
-- gunzip ; tar -xvf creates a directory "qepcad-linux". Let us say the full pathname is "/base-directory/qepcad-linux"

Step 2: Run the following command 

 -- /base-directory/qepcad-linux/install   /saclib-base-directory/saclib2.1  /base-directory/qepcad-linux

Note: This will take around 4 minutes. NOTE: need make-3.79.1 or newer version of make. Some old versions give an error.

Step 3: Test
-- Check if you have successfully created the libraries /base-directory/qepcad-linux/SFext/libsfext.a and /base-directory/qepcad-linux/source/libqepcad.a
-- Check if you have successfully created the executable /base-directory/qepcad-linux/source/qepcad

Download SAL (LISP only)

Download the gzipped tar file from here for SAL (over PVS/Lisp only), and follow the following instructions to install QEPCAD :

Step 1: Uncompress the file
Step 2: Make sure pvs3.0 is installed and that the file sal/sal/Sal points to it correctly.
Step 3: Run sal by calling sal/Sal

Download SAL Symbolic Simulation, Invariant Generation Routines

Download the gzipped tar file from here for SAL analysis routines, and follow the following instructions to install QEPCAD (see README file in there):

Step 1: Uncompress the file
Step 2: Make sure simulate.lisp has correct pathnames OR just run ./install with the correct directory path names.
Step 3: Load "simulate.lisp" into SAL/PVS/Lisp interface.
Step 4: Typecheck a SAL specification (javac/java needed).
Step 5: Use analysis tool on context/module selection.

Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page