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. Copyright 2006 ACM.
Author supplied keywords
Cite
CITATION STYLE
Siegel, S. F., Mironova, A., Avrunin, G. S., & Clarke, L. A. (2006). Using model checking with symbolic execution to verify parallel numerical programs. In Proceedings of the 2006 International Symposium on Software Testing and Analysis, ISSTA 2006 (Vol. 2006, pp. 157–167). https://doi.org/10.1145/1146238.1146256
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
