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/6920
Title: Verification Conditions for $\omega$-Automata and Applications to Fairness
Authors: Klarlund, Nils
Keywords: computer science
technical report
Issue Date: Feb-1990
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1080
Abstract: We present sound and complete verification conditions for proving that a program satisfies a specification definied by a deterministic Rabin automaton. Our verification conditions yield a simple method for proving that a program terminates under general fairness constraints. As opposed to previous approaches, our method is syntax-independent and does not require recursive applications of proof rules. Moreover using a result by Safra, we obtain the first direct method for proving that a program satisfies a Buchi automaton specification. Finally, we show that our method generalized two earlier methods.
URI: http://hdl.handle.net/1813/6920
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
90-1080.pdf2.82 MBAdobe PDFView/Open
90-1080.ps596.64 kBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us