Seminars & Events

Mathematics and Computer Science Division
"Formal Specification and Verification of MPI Programs Using TASS"

DATE: March 31, 2011 to March 31, 2011
TIME: 10:30 AM - 11:30 AM
SPEAKER: Stephen F. Siegel, Assistant Professor, Verified Software Laboratory, University of Delaware
LOCATION: Building 240 Conference Center Room 1404, Argonne National Laboratory
HOST: Rusty Lusk

Description:
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.

Save the event to your calendar [schedule.ics]