This set of examples demonstrate using CIVL to compare the functional
equivalence of two programs.

The folder dotprod contains four different implementations of dot
product computation, which are sequential, MPI, Pthreads, and hybrid
MPI+Pthreads. CIVL is able to compare any of the two implementations
and prove their funtional equivalence.

The folder forward contains two different implementations of forward
difference gradient approximator, both of which are sequential
programs. One is written manually and the other is generated by a tool
call ADIC.  CIVL finds that there is a possible division by 0 error of
the programs. After fixing that (by adding an assumption that the
corresonding expression not equal to 0), CIVL is able to prove the
functional equivalence of both implementation.
