Combining symbolic execution with model checking to verify parallel numerical programs
Abstract
We present a method to verify the correctness of parallel programs that perform complex numerical computations, including computations involving floating-point arithmetic. This method requires that a sequential version of the program be provided, to serve as the specification for the parallel one. The key idea is to use model checking, together with symbolic execution, to establish the equivalence of the two programs. In this approach the path condition from symbolic execution of the sequential program is used to constrain the search through the parallel program. To handle floating-point operations, three different types of equivalence are supported. Several examples are presented, demonstrating the approach and actual errors that were found. Limitations and directions for future research are also described.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Apr 01, 2008
- Source ID
- 10.1145/1348250.1348256
Entities
People
- Anastasia Mironova
- George S. Avrunin
- Lori A. Clarke
- Stephen F. Siegel
Organizations
- Army Research Office
- Division of Computing and Communication Foundations
- National Science Foundation
- University of Delaware
- University of Massachusetts
- University of Utah