Using model checking with symbolic execution to verify parallel numerical programs

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.

• Type: Conference
• Year: 2006
• Where: ISSTA
• Authors: Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, Lori A. Clarke
• Keywords: Complex Numerical Computations, ISSTA 2006, Parallel Programs, Sequential Version