Now showing items 1-8 of 8

• #### Convergence Measures ﻿

(Cornell University, 1990-03)
General methods of verification for programs defining infinite computataions rely on measuring progress or convergence of finite computations towards satisfying the specification. Traditionally, progress is measured using ...
• #### Limit Operators and Convergence Measures for $\omega$-Languages with Applications to Extreme Fairness ﻿

(Cornell University, 1990-02)
Methods of program verification for liveness and fairness rely on measuring "progress" of finite computations towards satisfying the specification. Previous methods are based on explaining progress in terms of well-founded ...
• #### Progress Measures and Finite Arguments for Infinite Computation ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ...