Towards Deductive Verification of Message-Passing Parallel Programs

Program verification techniques based on deductive reasoning can provide a very high level of assurance of correctness. These techniques are capable of proving correctness without placing artificial bounds on program parameters or on the sizes of inputs. While there are a number of mature frameworks for deductive verification of sequential programs, there is much less for parallel programs, and very little for message-passing. We propose a method for the deductive verification of message-passing programs that involves transforming the program into an annotated sequential program that can be verified with off-the-shelf deductive tools, such as Frama-C. The method can prove user-specified correctness properties without any bounds on the number of processes or other parameters. We illustrate this method on a toy example, and analyze its strengths and weaknesses.

@inproceedings{luo-siegel:2018:correctness,
  author = {Ziqing Luo and Stephen F.\ Siegel},
  title = {Towards Deductive Verification of Message-Passing
           Parallel Programs},
  booktitle = {2018 IEEE/ACM 2nd International Workshop on Software
                  Correctness for HPC Applications (Correctness)},
  editor = {Ignacio Laguna and Cindy Rubio-Gonz\'alez},
  year = {2018},
  publisher = {IEEE},
  doi = {10.1109/Correctness.2018.00012}
}