TASS: The Toolkit for Accurate Scientific Software

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 .