Now showing items 3-8 of 8

    • Progress Measures and Finite Arguments for Infinite Computation 

      Klarlund, Nils (Cornell University, 1990-09)
      We 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, ...
    • Progress Measures for Verification Involving Nondeterminism 

      Klarlund, Nils; Schneider, Fred B. (Cornell University, 1990-11)
      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 ...
    • Proving Nondeterministically Specified Safety Properties Using Progress Measures 

      Klarlund, Nils; Schneider, Fred B. (Cornell University, 1991-05)
      Using the notion of progress measures, we discuss verification methods for proving that a program satisfies a property specified by an automaton having finite nondeterminism. Such automata can express any safety property. ...
    • Rabin Measures and Their Applications to Fairness and Automata Theory 

      Klarlund, Nils; Kozen, Dexter (Cornell University, 1991-04)
      Rabin conditions are general class of properties of infinite sequences that emcompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper we show how to determine whether a program ...
    • Verification Conditions for $\omega$-Automata and Applications to Fairness 

      Klarlund, Nils (Cornell University, 1990-02)
      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 ...
    • Verifying Safety Properties Using Non-deterministic Infinite-state Automata 

      Klarlund, Nils; Schneider, Fred B. (Cornell University, 1989-09)
      A new class of infinite-state automata, called safety automata, is introduced. Any safety property can be specified by using such an automaton. Sound and complete proof obligations for establishing that an implementation ...