Stephen F. Siegel and Timothy K. Zirkel,
Mathematics
in Computer Science 5(4):395–426, 2011.

The Toolkit for Accurate Scientific Software (TASS) is a suite
of integrated tools for the formal verification of programs
used in computational science, including numerically-intensive
message-passing-based parallel programs. While TASS can
verify a number of standard safety properties (such as absence
of deadlocks and out-of-bound array indexing), its most
powerful feature is the ability to establish that two programs
are functionally equivalent. These properties are verified by
performing an explicit state enumeration of a model of the
program(s). In this model, symbolic expressions are used to
represent the inputs and the values of variables. TASS uses
novel techniques to simplify the symbolic representation of
the state and to reduce the number of states explored and
saved. The TASS front-end supports a large subset of C,
including (multi-dimensional) arrays, structs, dynamically
allocated data, pointers and pointer arithmetic, functions and
recursion, and other commonly used language constructs. A
number of experiments on small but realistic numerical
programs show that TASS can scale to reasonably large
configurations and process counts. TASS is open source
software distributed under the GNU Public License. The Java
source code, examples, experimental results, and reference
materials are all available at
http://vsl.cis.udel.edu/tass.

- tass_tr_2011.pdf (preprint)
- tass_tr_2011.tgz (gzipped tar archive of experimental data)

@article{siegel-zirkel:2011:tass-mcs, Author = {Stephen F. Siegel and Timothy K. Zirkel}, Journal = {Mathematics in Computer Science}, Number = {4}, Pages = {395--426}, Publisher = {Birkh\"auser Basel}, Title = {{TASS}: The {T}oolkit for {A}ccurate {S}cientific {S}oftware}, Volume = {5}, Year = {2011}}

VSL | Publications