The   Toolkit   for   Accurate   Scientific   Software  
  1. Overview
  2. Download and installation
  3. Documents
  4. E-mail Lists
  5. Developer Links
  6. Usage
  7. Examples
  8. License

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.

Download and Installation

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:

  1. The Toolkit for Accurate Scientific Software (Technical Report, 31 pages)
  2. Automatic Formal Verification of MPI-Based Parallel Programs (PPoPP 2011, 2 pages)
  3. Collective Assertions (VMCAI 2011, 16 pages)
  4. Symbolic Execution for Sequential and Multi-Process Programs with Unbounded Loops (Technical Report, 17 pages)
E-mail Lists
  1. TASS Users: a list for users of TASS, general discussion, problems, bug reports, etc. Open to all.
  2. TASS Developers: a list for the developers of TASS.
Developer Links
  1. Javadoc API
  2. Trac site
  3. JUnit Test Results (run after each commit)
  4. Jacoco Coverage Report
  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

-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
    specify concrete initial value for input variable VARIABLE
  1. Diffusion Solver
  2. Grade Counter
  3. LaPlace Equation Solver

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.