Incremental verification of Owicki/Gries proof outlines using PVS

Abstract. Verifications of parallel programs are frequently based on automated state-space exploration techniques known as model checking. To avoid state-space explosion problems, theorem proving techniques can be used, for example by manually annotating programs with suitable as-sertions and using these assertions to prove their correctness (e.g. using the Owicki/Gries theory). We propose a method to support assertion-based methods with theorem provers like PVS. Emphasis is on the typi-cal incremental character of assertion-based methods, and on automated strategies for proving correctness of the proof outlines.