A survey of verification techniques for parallel programs (Q1059388)

This report is an attempt at trying to document some of the many verification methods for parallel and distributed software. Preliminary aims were that the report should highlight common ideas, principles and implications of current verification and specification techniques. Neither this report is meant to be an all embracing survey report. Some of the main approaches in this area are reviewed and studied in grater depth. The following scheme is used for the presentation of each method: Major references, Overview, Examples, Detailed exposition of some examples, General comments and a summary of the proof system. There are two main sections to the report: Shared variable parallelism and Message- based parallelism. In detail the following methods are surveyed: Flon \& Suzuki: Total Correctness of Parallel Programs; Jones: Development of Interfering Programs; Lamport: Verification of Concurrent Programs; Owicki \& Gries: Verification of Parallel Programs; Apt, Francez \& De Roever: Verification of CSP; Barringer \& Mearns: Verification of Ada Tasks; Levin \& Gries: Verification of CSP; Misra \& Chandy: Proofs of Process Networks; Zhou \& Hoare: Correctness of Communicating Processes.