<span class="var-sub_title">Toward Deductive Verification of Message-Passing Parallel Programs</span> SC18 Proceedings

The International Conference for High Performance Computing, Networking, Storage, and Analysis

2nd International Workshop on Software Correctness for HPC Applications (Correctness 2018)


Toward Deductive Verification of Message-Passing Parallel Programs

Authors: Ziqing Luo (University of Delaware)

Abstract: 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.

Archive Materials


Back to 2nd International Workshop on Software Correctness for HPC Applications (Correctness 2018) Archive Listing

Back to Full Workshop Archive Listing