Using model checking with symbolic execution to verify parallel numerical programs

  • Siegel S
  • Mironova A
  • Avrunin G
 et al. 
  • 30


    Mendeley users who have this article in their library.
  • 34


    Citations of this article.


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.

Author-supplied keywords

  • MPI
  • concurrency
  • finite state verification
  • floating-point
  • high performance computing
  • message passing interface
  • model checking
  • numerical program
  • parallel programming
  • spin
  • symbolic execution

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Stephen F Siegel

  • Anastasia Mironova

  • George S Avrunin

  • Lori A Clarke

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free