Now showing items 63-82 of 101

    • On Restrictions to Ensure Reproducible Behavior in Concurrent Programs 

      Schneider, Fred B.; Bernstein, A. J. (Cornell University, 1979-03)
      One of the major difficulties encountered when dealing with concurrent programs is that reproducible behavior may not be assumed. As a result, it is difficult to validate and debug such systems. In this paper, structural ...
    • Operating System Support for Mobile Agents 

      Johansen, Dag; Van Renesse, Robbert; Schneider, Fred B. (Cornell University, 1994-12)
      An "agent" is a process that may migrate through a computer network in order to satisfy requests made by its clients. Agents implement a computational metaphor that is analogous to how most people conduct business in their ...
    • Optimal Primary-Backup Protocols 

      Budhiraja, Navin; Marzullo, Keith; Schneider, Fred B.; Toueg, Sam (Cornell University, 1992-08)
      We give primary-backup protocols for various models of failure. These protocols are optimal with respect to degree of replication, failover time, and response time to client requests.
    • A Paradigm for Reliable Clock Synchronization 

      Schneider, Fred B. (Cornell University, 1986-02)
      Existing fault-tolerant clock synchronization protocols are shown to result from refining a single clock synchronization paradigm. In that paradigm, a reliable time source periodically issues messages that cause processors ...
    • Peer-to-Peer Authentication with a Distributed Single Sign-On Service 

      Josephson, William; Sirer, Emin Gun; Schneider, Fred B. (Cornell University, 2004-02-16)
      CorSSO is a distributed service for authentication in networks. It allows application servers to delegate client identity checking to combinations of authentication servers potentially residing in separate administrative ...
    • Personal Keys, Group Keys and Master Keys 

      Denning, Dorothy E.; Schneider, Fred B. (Cornell University, 1980-01)
    • Pretending Atomicity 

      Lamport, Leslie; Schneider, Fred B. (Cornell University, 1989-05)
      We present a theorem for deriving properties of a concurrent program by reasoning about a simpler, coarser-grained version. The theorem generalizes a result that Lipton proved for partial correctness and deadlock-freedom. ...
    • Primary-Backup Protocols: Lower Bounds and Optimal Implementations 

      Budhiraja, Navin; Marzullo, Keith; Schneider, Fred B.; Toueg, Sam (Cornell University, 1992-01)
      We present a formal specification of primary-backup. We then prove lower bounds on the degree of replication, failover time and worst-case response time to client requests assuming different failure models. Finally, we ...
    • Proactive Obfuscation 

      Roeder, Tom; Schneider, Fred B. (2009-03-28)
      Proactive obfuscation is a new method for creating server replicas that are likely to have fewer shared vulnerabilities. It uses semantics-preserving code transformations to generate diverse executables, periodically ...
    • 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 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 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. ...
    • Putting Time into Proof Outlines 

      Schneider, Fred B.; Bloom, Bard; Marzullo, Keith (Cornell University, 1991-09)
    • Quantification of Integrity 

      Clarkson, Michael R.; Schneider, Fred B. (2011-01-12)
      Three integrity measures are introduced: contamination, channel suppression, and program suppression. Contamination is a measure of how much untrusted information reaches trusted outputs; it is the dual of leakage, which ...
    • Quantifying Information Flow with Beliefs 

      Clarkson, Michael R.; Myers, Andrew C.; Schneider, Fred B. (Cornell University, 2007-03-01)
      To reason about information flow, a new model is developed that describes how attacker beliefs change due to the attacker's observation of the execution of a probabilistic (or deterministic) program. The model enables ...
    • Reasoning About Programs by Exploiting the Environment 

      Fix, Limor; Schneider, Fred B. (Cornell University, 1994-02)
      A method for making aspects of a computational model explicit in the formulas of a programming logic is given. The method is based on a new notion of environment -- an environment augments the state transitions defined ...
    • 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 ...
    • Refinement for Fault-Tolerance: An Aircraft Hand-off Protocol 

      Marzullo, Keith; Schneider, Fred B.; Dehn, Jon (Cornell University, 1994-04)
      Part of the Advanced Automation System (AAS) for air-traffic control is a protocol to permit flight hand-off from one air-traffic controller to another. The protocol must be fault-tolerant and, therefore, is subtle--an ...
    • 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 ...
    • SASI Enforcement of Security Policies: A Retrospective 

      Erlingsson, Ulfar; Schneider, Fred B. (Cornell University, 1999-07)
      SASI enforces security policies by modifying object code for a target system before that system is executed. The approach has been prototyped for two rather different machine architectures: Intel x86 and Java JVML. Details ...