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 assertions 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 typical incremental character of assertion-based methods, and on automated strategies for proving correctness of the proof outlines.
|Title of host publication||Formal methods and software engineering : 7th international conference, ICFEM 2005, Manchester, UK, November 1-4, 2005 : proceedings|
|Editors||K.K. Lau, R. Banach|
|Place of Publication||Berlin|
|Publication status||Published - 2005|
|Name||Lecture Notes in Computer Science|