@inproceedings{9604cdcafb014afd86dd58240c2f741e,
title = "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 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.",
author = "A.J. Mooij and J.W. Wesselink",
year = "2005",
doi = "10.1007/11576280_27",
language = "English",
isbn = "3-540-29797-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "390--404",
editor = "K.K. Lau and R. Banach",
booktitle = "Formal methods and software engineering : 7th international conference, ICFEM 2005, Manchester, UK, November 1-4, 2005 : proceedings",
address = "Germany",
}