VSL Publications

Towards Deductive Verification of Message-Passing Parallel Programs

Ziqing Luo and Stephen F. Siegel. Towards Deductive Verification of Message-Passing Parallel Programs. In Proceedings of the 2nd International Workshop on Software Correctness for HPC Applications
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.
  1. Under Construction
Related Links
  1. Experimental Archive page
		  Under Construction

VSL | Publications