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 computation, to establish the equivalence of the two programs.
This paper appeared as Technical Report UM-CS-2005-15, Department of Computer Science, University of Massachusetts, 2005.
The conference version appeared in Proceedings of the ACM SIGSOFT 2006 International Symposium on Software Testing and Analysis, Portland, ME, USA, July 17-20, 2006, pages 157-167.
You may download the paper in one of the following formats:
Other items: