The International Conference for High Performance Computing, Networking, Storage, and Analysis
The International Conference for High Performance Computing, Networking, Storage, and Analysis
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