Now showing items 5-7 of 7

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