Now showing items 1-7 of 7

    • Defining Liveness 

      Alpern, Bowen; Schneider, Fred B. (Cornell University, 1985-10)
      A formal definition for liveness properties is proposed. It is argued that this definition captures the intuition that liveness properties stipulate that "something good" eventually happens during execution. A topological ...
    • Key Exchange Using Keyless Cryptography 

      Alpern, Bowen; Schneider, Fred B. (Cornell University, 1982-08)
      Protocols to generate and distribute secret keys in a computer network are described. They are based on keyless cryptography, a new cryptographic technique where information is hidden by keeping only the originator of a ...
    • Proving Boolean Combinations of Deterministic Properties 

      Alpern, Bowen; Schneider, Fred B. (Cornell University, 1987-03)
      This paper gives a method for providing that a program satisfies a temporal property that has been specified in terms of Buchi automata. The method permits extraction of proof obligations for a property formulated as the ...
    • Proving Temporal Properties of Concurrent Programs: A Non-Temporal Approach 

      Alpern, Bowen (Cornell University, 1986-02)
      This thesis develops a new method for proving properties of concurrent programs and gives formal definitions for safety and liveness. A property is specified by a property recognizer - a finite-state machine that accepts ...
    • Recognizing Safety and Liveness 

      Alpern, Bowen; Schneider, Fred B. (Cornell University, 1986-01)
      Formal characterizations for safety properties and liveness properties are given in terms of the structure of the Buchi automaton that specifies the property. The characterizations permit a property to be decomposed into ...
    • Safety Without Stuttering 

      Alpern, Bowen; Demers, Alan J.; Schneider, Fred B. (Cornell University, 1985-10)
      A new formalization of safety properties is given. The formalization agrees with the informal definition - that a safety property stipulates that some "bad thing" doesn't happen during execution - for properties that are ...
    • Verifying Temporal Properties without using Temporal Logic 

      Alpern, Bowen; Schneider, Fred B. (Cornell University, 1987-07)
      An approach to proving temporal properties of concurrent programs that does not use temporal logic as an inference system is presented. The approach is based on using Buchi automata to specify properties. To show that a ...