Skip to main content


eCommons@Cornell

eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/7190
Title: A Consistent and Complete Deductive System for the Verification of Parallel Programs
Authors: Owicki, Susan S.
Keywords: computer science
technical report
Issue Date: May-1976
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR76-278
Abstract: The semantics of a simple parallel programming language is presented in two ways: deductively, by a set of Hoare-like axioms and inference rules, and operationally, by means of an interpreter. It is shown that the deductive system is consistent with the interpreter. It would be desirable to show that the deductive system is also complete with respect to the interpreter, but this is impossible since the programming language contains the natural numbers. Instead it is proven that the deductive system is complete relative to a complete proof system for the natural numbers; this result is similar to Cook's relative completeness for sequential programs. The deductive semantics given here is an extension of an incomplete deductive system proposed by Hoare. The key difference is an additional inference rule which provides for the introduction of auxiliary variables in a program to be verified.
URI: http://hdl.handle.net/1813/7190
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
76-278.pdf1.83 MBAdobe PDFView/Open
76-278.ps454.15 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us