Incremental verification of Owicki/Gries proof outlines using PVS

A.J. Mooij, J.W. Wesselink

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationFormal methods and software engineering : 7th international conference, ICFEM 2005, Manchester, UK, November 1-4, 2005 : proceedings
EditorsK.K. Lau, R. Banach
Place of PublicationBerlin
PublisherSpringer
Pages390-404
ISBN (Print)3-540-29797-9
DOIs
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
Volume3785
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Incremental verification of Owicki/Gries proof outlines using PVS'. Together they form a unique fingerprint.

Cite this