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. The 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.

Appeared in

Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, July 17--20, 2006, Lori L. Pollock and Mauro Pezze, editors, ACM, pages 157-168.

BibTeX

@InProceedings{siegel-mironova-avrunin-clarke:2006:symbolic,
  author = "Stephen F. Siegel and Anastasia Mironova and George S. Avrunin and Lori A. Clarke",
  title = "Using Model Checking with Symbolic Execution to Verify Parallel Numerical Programs",
  crossref = {issta2006},
  pages = {157--168}
}
@Proceedings{issta2006,
  booktitle = {Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis,
               ISSTA 2006, Portland, Maine, USA, July 17--20, 2006},
  title = {Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, 
           ISSTA 2006, Portland, Maine, USA, July 17--20, 2006},
  editor = {Lori L.\ Pollock and Mauro Pezz\'e},
  publisher = {ACM},
  year = 2006
}

Download

Related Links