Here is 2 message-passing programs that can be verified by both TASS and CIVL via 
comparing the parallel version of the program with a sequential version.

The structure of the folder is:
TASS/
  adder/
    adder_seq.c            /* sequential adder program used by TASS compare */
    adder_par.c            /* parallel  adder program used by TASS compare */
    CIVL/
      adder_spec.c         /* sequential adder program used by CIVL compare */
      adder_par.c          /* parallel adder program used by CIVL compare */
  diffusion1d/
    diffusion_seq.c        /* sequential diffusion-1d program used by TASS compare */
    diffusion_par.c        /* parallel diffusion-1d program used by TASS compare */
    CIVL/
      diffusion1d_spec.c   /* sequential diffusion-1d program used by TASS compare */
      diffusion1d_par.c    /* parallel diffusion-1d program used by TASS compare */

To run the comparison: Type "make" under each folder. 
Or using CIVL and TASS commands to run the program.
TASS can be downloaded at http://vsl.cis.udel.edu/tass/index.html
