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/6085
Title: Notes on Proof Outline Logic
Authors: Schneider, Fred B.
Keywords: computer science
technical report
Issue Date: Jan-1995
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR95-1476
Abstract: Formulas of Proof Outline Logic are program texts annotated with assertions. Assertions may contain control predicates as well as terms whose values depend on previous states, making the assertion language rather expressive. The logic is complete for proving safety properties of concurrent programs. A deductive system for the logic is presented. Solutions to the mutual exclusion and readers/writers problems illustrate how the logic can be used as a tool for program development.
URI: http://hdl.handle.net/1813/6085
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
95-1476.pdf156.17 kBAdobe PDFView/Open
95-1476.ps326.95 kBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us