JavaScript is disabled for your browser. Some features of this site may not work without it.
Progress Measures for Verification Involving Nondeterminism

Author
Klarlund, Nils; Schneider, Fred B.
Abstract
Using the notion of progress measures, we give a complete verification method for proving that a program satisfies a property specified by an automaton having bounded nondeterminism. Such automata can express any safety property. Previous methods, which can be derived from the method presented here, either rely on transforming the program or are not complete.
Date Issued
1990-11Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1167
Type
technical report