Authors
Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, and Lori A. Clarke
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.
Appeared in
ACM Transactions on Software Engineering and Methodology 17(2), Article 10, 2008, 1-34.
BibTeX
@Article{siegel-mironova-avrunin-clarke:2008:tosem,
author = "Stephen F. Siegel and Anastasia Mironova and George S. Avrunin and Lori A. Clarke",
title = "Combining Symbolic Execution with Model Checking to Verify Parallel Numerical Programs",
journal = "ACM Transactions on Software Engineering and Methodology",
year = 2008,
pages = {Article 10, 1--34},
volume = 17,
number = 2
}
Download
- http://vsl.cis.udel.edu/downloads/symbolic_tosem_2008.pdfsymbolic_tosem_2008.pdf (full paper)
- http://vsl.cis.udel.edu/downloads/symbolic_tosem_2008.tgzsymbolic_tosem_2008.tgz (examples used in paper)
