Stephen F. Siegel and Timothy K. Zirkel, A
Functional Equivalence Verification Suite for High-Performance
Scientific Computing. Mathematics
in Computer Science 5(4):427–435, 2011.

Scientific computing poses many challenges to formal
verification, including the facts that typical programs (1)
are numerically-intensive, (2) are highly-optimized (often by
hand), and (3) often employ parallelism in complex ways.
Another challenge is specifying correctness. One approach is
to provide a very simple, sequential version of an algorithm
together with the optimized (possibly parallel) version. The
goal is to show the two versions are functionally equivalent,
or provide useful feedback when they are not. We present a
new verification suite consisting of pairs of programs of this
form. The suite can be used to evaluate and compare tools
that verify functional equivalence. The programs are all in C
and the parallel versions use the Message Passing Interface.
They are simpler than codes used in practice, but are
representative of real coding patterns (e.g., manager-worker
parallelism, loop tiling) and present realistic challenges to
current verification tools. The suite includes solvers for
the 1-d and 2-d diffusion equations, Jacobi iteration schemes,
Gaussian elimination, and N-body simulation.

- fevs_tr_2011.pdf (preprint)

@article{siegel-zirkel:2011:fevs-mcs, Author = {Stephen F. Siegel and Timothy K. Zirkel}, Journal = {Mathematics in Computer Science}, Number = {4}, Pages = {427--435}, Publisher = {Birkh\"auser Basel}, Title = {{FEVS}: A {F}unctional {E}quivalence {V}erification {S}uite for High Performance Scientific Computing}, Volume = {5}, Year = {2011}}

VSL | Publications