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/6688
Title: Verifying Temporal Properties without using Temporal Logic
Authors: Alpern, Bowen
Schneider, Fred B.
Keywords: computer science
technical report
Issue Date: Jul-1987
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-848
Abstract: An approach to proving temporal properties of concurrent programs that does not use temporal logic as an inference system is presented. The approach is based on using Buchi automata to specify properties. To show that a program satisfies a given property, proof obligations are derived from the Buchi automaton for that property. These obligations are discharged by devising suitable invariant assertions and variant functions for the program. The approach is shown to be sound and relatively complete. A mutual exclusion protocol illustrates its application.
URI: http://hdl.handle.net/1813/6688
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
87-848.pdf2.05 MBAdobe PDFView/Open
87-848.ps569.8 kBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us