The Toolkit for Accurate Scientific Software (TASS, http://vsl.cis.udel.edu/tass) is a new symbolic execution framework for verifying C/MPI programs. TASS can verify that a program is free of deadlocks, buffer overflows, memory leaks, null pointer dereferences, divisions by 0, and assertion violations, within a bounded region of the program's input space. In addition, it can compare two programs to determine whether they are functionally equivalent. This allows the developer to use a simple sequential program as a specification and use TASS to show that a more complex, parallel program is a correct implementation of that specification. TASS is being used to explore other specification mechanisms, such as "collective assertions" that span multiple processes. Unlike previous tools, such as MPI-Spin, TASS works directly from C source code, augmented with a minimal amount of user annotations. A number of novel model checking optimizations have also been incorporated, allowing TASS to scale much further than previous approaches.