Now showing items 58-77 of 101

    • NAP: Practical Fault-Tolerance for Itinerant Computations 

      Johansen, Dag; Marzullo, Keith; Schneider, Fred B.; Jacobsen, Kjetil; Zagorodnov, Dmitrii (Cornell University, 1998-11)
      NAP, a detection and recovery based scheme for implementing fault-tolerant itinerant computations, is presented. We give the semantics for the scheme and describe a protocol that implements NAP in Tacoma.
    • NAP: Practical Fault-Tolerance for Itinerant Computations 

      Johansen, Dag; Marzullo, Keith; Schneider, Fred B.; Jacobsen, Kjetil; Zagorodnov, Dmitrii (Cornell University, 1999-03)
      NAP is a protocol for supporting fault-tolerance in intinerant computations. It employs a form of failure detection and recovery, and it generalizes the primary-backup approach to a new compuational model. The guarantees ...
    • A New Approach to Teaching Mathematics 

      Gries, David; Schneider, Fred B. (Cornell University, 1994-02)
      We propose a new approach to teaching discrete math: First, teach logic as a powerful and versatile tool for discovering and communicating truths; then use this tool in all other topics of the course. We spend 6 weeks ...
    • Nexus Authorization Logic (NAL): Design Rationale and Applications 

      Schneider, Fred B.; Walsh, Kevin; Sirer, Emin Gun (2009-09-14)
      Nexus Authorization Logic (NAL) provides a principled basis for specifying and reasoning about credentials and authorization policies. It extends prior access control logics based on "says" and "speaksfor" operators, ...
    • Notes on Proof Outline Logic 

      Schneider, Fred B. (Cornell University, 1995-01)
      Formulas of Proof Outline Logic are program texts annotated with assertions. Assertions may contain control predicates as well as terms whose values depend on previous states, making the assertion language rather expressive. ...
    • 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)
      NO ABSTRACT SUPPLIED
    • 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 ...