Show simple item record

dc.contributor.authorKlarlund, Nilsen_US
dc.date.accessioned2007-04-23T17:49:37Z
dc.date.available2007-04-23T17:49:37Z
dc.date.issued1990-09en_US
dc.identifier.citationhttp://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1153en_US
dc.identifier.urihttps://hdl.handle.net/1813/6993
dc.description.abstractWe establish principles for proving properties about infinite computations by reasoning about finite ones. We apply these principles to show that for a wide variety of verification problems - involving nondeterminism, fairness, and liveness - there are assertional verification methods that directly relate program and specification. Most previous research relies on transformations of programs in order to reduce a verification problem to problems that can be solved using classical techniques such a refinement mappings and well-founded orderings. Progress measures, the key innovation of this thesis, provide direct, syntax-independent verification techniques for a wide range of specifications. We exhibit progress measures for the language containment problem for nondeterministic automata; for verification with general fairness constraints; and for verification of very general specifications, including infinitary temporal logics. We obtain and optimal solution (in a recursion-theoretic sense) to the problem of verifying infinite computations by reasoning about finite ones. This result establishes a link between descriptive set theory and the theory of verification.en_US
dc.format.extent7730616 bytes
dc.format.extent1651509 bytes
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.language.isoen_USen_US
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleProgress Measures and Finite Arguments for Infinite Computationen_US
dc.typetechnical reporten_US


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Statistics