TASS is a suite of integrated tools for the formal verification of programs used in computational science, including message-passing-based parallel programs. TASS uses symbolic execution and model checking techniques to verify a number of standard safety properties (such as absence of deadlocks and out-of-bound references), but its most innovative feature is the ability to establish that two programs are functionally equivalent. This is particularly useful in scientific computing, where developers often start with a simple sequential encoding of an algorithm, then gradually transform this into a production code by introducing parallelism and a host of other optimizations by hand. The final implementation is intended to be functionally equivalent to the original specification, but this is generally extremely difficult to check.
TASS is developed by the Verified Software Laboratory, under the direction of Stephen Siegel.
TASS is supported by the U.S. National Science Foundation grant CCF-0733035.
TASS is open source software distributed under the GNU Public License.
The current version of TASS is 1.2. Installation instructions can be found in the README file included in the distribution.
Each link brings you to a page for the paper and related experimental artifacts:
Usage:
tass help
tass verify [options] model.c
tass compare [options] spec.c impl.c
tass replay [options] name.trace
Description of sub-commands:
help: print this message
verify: verify safety properties hold for one program
compare: verify functional equivalence of two programs
replay: replay trace generated from previous run
Options:
-buffer=INTEGER (default: 10)
upper bound on total number of buffered messages
-ca or -ca=BOOLEAN (default: false)
check collective assertions
-cqmin or -cqmin=BOOLEAN (default: true)
use collective queue minimization heuristic
-detectCycles or -detectCycles=BOOLEAN (default: false)
report cycles in state space as errors
-deadlock=STRING (default: absolute)
deadlock detection: ignore, absolute, or potential
-debug or -debug=BOOLEAN (default: false)
print very detailed output
-drawgraph or -drawgraph=BOOLEAN (default: false)
draw graph of reachable state space
-errorBound=INTEGER (default: 1)
upper bound on number of errors found before quitting
-loop or -loop=BOOLEAN (default: false)
use collective loop invariant technique
-np=INTEGER (default: 1)
number of processes in verify run
-np1=INTEGER (default: 1)
number of processes in specification (compare mode only)
-np2=INTEGER (default: 1)
number of processes in implementation (compare mode only)
-reduce=STRING (default: urgent)
partial order reduction strategy: std or urgent
-showModel or -showModel=BOOLEAN (default: false)
print the model(s) extracted from source
-showProverQueries or -showProverQueries=BOOLEAN (default: false)
show queries passed to theorem prover
-showQueries or -showQueries=BOOLEAN (default: false)
show all queries
-showSavedStates or -showSavedStates=BOOLEAN (default: false)
show saved states only
-showSimplifications or -showSimplifications=BOOLEAN (default: false)
show results of symbolic simplifications
-showStates or -showStates=BOOLEAN (default: false)
show all states
-showTransitions or -showTransitions=BOOLEAN (default: false)
show transitions
-simplify or -simplify=BOOLEAN (default: true)
simplify saved states and predicates
-verbose or -verbose=BOOLEAN (default: false)
verbose output
-inputVARIABLE=VALUE
specify concrete initial value for input variable VARIABLE
TASS is copyright 2010-2011, Verified Software Laboratory, University of Delaware
This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this program. If not, see here.