Now showing items 81-100 of 101

    • 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 ...
    • Simpler Proofs for Concurrent Reading and Writing 

      Schneider, Fred B. (Cornell University, 1989-09)
      Simplified proofs are given for Lamport's protocol to coordinate concurrent reading and writing.
    • The State Machine Approach: A Tutorial 

      Schneider, Fred B. (Cornell University, 1986-12)
      The state machine approach is a general method for achieving fault tolerance and implementing decentralized control in distributed systems. This paper reviews the approach and identifies abstractions needed for coordinating ...
    • Supporting Broad Internet Access to TACOMA 

      Johansen, Dag; van Renesse, Robbert; Schneider, Fred B. (Cornell University, 1996-07)
      Any provider of software is faced with a problem if that software must be installed on autonomous sites of a large network. This paper reports experiences in addressing this network-software installation- problem for ...
    • Symmetry and Similarity in Distributed Systems 

      Johnson, Ralph E.; Schneider, Fred B. (Cornell University, 1985-05)
      Similarity is introduced as a model-independent characterization of symmetry. It can be used to decide when a concurrent system has a solution to the selection problem. It can also be used to compare different models of ...
    • Synchronization in Distributed Programs 

      Schneider, Fred B. (Cornell University, 1979-09)
      A technique for solving synchronization problems in distributed programs is described. Use of this technique in environments in which processes may fail is discussed. The technique can be used to solve synchronization ...
    • A TACOMA Retrospective 

      Johansen, Dag; Lauvset, Kare J.; van Renesse, Robbert; Schneider, Fred B.; Sudmann, Nils P.; Jacobsen, Kjetil (Cornell University, 2001-12-04)
      For seven years, the TACOMA project has investigated the design and implementation of software support for mobile agents. A series of prototypes has been developed, with experiences in distributed applications driving the ...
    • Teaching Math More Effectively, Through the Design of Calculational Proofs 

      Gries, David; Schneider, Fred B. (Cornell University, 1994-03)
      Lower-level college math courses usually avoid using formalism, in both definitions and proofs. Later, when students have mastered definitions and proofs written largely in English, they may be shown how informal reasoning ...
    • Three Surveys on Operating System Topics 

      Andrews, Gregory R.; Schneider, Fred B. (Cornell University, 1980-05)
      Recently, we were asked by the Wiley Publishing Company to write survey articles covering some of the important concepts in operating systems for their forthcoming Handbook of Electrical and Computer Engineering. The ...
    • Thrifty Execution of Task Pipelines 

      Schneider, Fred B.; Conway, Richard W.; Skeen, Dale (Cornell University, 1984-06)
      A sequence of tasks that must be performed on a sequential database can be scheduled in various ways. Schedules will differ with respect to the number of accesses made to peripheral storage devices and the amount of ...
    • Tolerating Malicious Gossip 

      Minsky, Yaron M.; Schneider, Fred B. (Cornell University, 2001-10-08)
      A new class of gossip protocols is presented to diffuse updates securely. The protocols rely on annotating updates with the path along which they travel. To avoid a combinatorial explosion in the number of such annotated ...
    • Towards Fault-tolerant and Secure Agentry 

      Schneider, Fred B. (Cornell University, 1997-07)
      Processes that roam a network--agents--present new technical challenges. Two are discussed here. The first problem, which arises in connection with implementing fault-tolerant agents, concerns how a voter authenticates ...
    • Trace-Based Network Proof Systems: Expressiveness and Completeness 

      Widom, Jennifer; Gries, David; Schneider, Fred B. (Cornell University, 1989-02)
      We consider incomplete trace-based network proof systems for safety properties, identifying extensions that are necessary and sufficient to achieve relative completeness. We then consider the expressiveness required of ...
    • Understanding Protocols for Byzantine Clock Synchronization 

      Schneider, Fred B. (Cornell University, 1987-08)
      All published fault-tolerant clock synchronization protocols are shown to result from refining a single paradigm. This allows the different clock synchronization protocols to be compared and permits presentation of a ...
    • User Recovery and Reversal in Interactive Systems 

      Archer, James E. Jr.; Conway, Richard W.; Schneider, Fred B. (Cornell University, 1981-10)
      Interactive systems, such as editors and program development environments, should be explicitly support recovery - facilities that permit a user to reverse the effects of past actions and to restore an object to a prior ...
    • Using Message Passing for Distributed Programming: Proof Rules and Disciplines 

      Schlichting, Richard D.; Schneider, Fred B. (Cornell University, 1982-05)
      Inference rules are derived for proving partial correctness of concurrent programs that use message passing. These rules extend the notion of a satisfaction proof, first proposed for proving correctness of programs that ...
    • Verifying Programs That Use Causally-Ordered Message-Passing 

      Stoller, Scott D.; Schneider, Fred B. (Cornell University, 1994-05)
      We give an operational model of causally-ordered message-passing primitives. Based on this model, we formulate a Hoare-style proof system for causally-ordered delivery. To illustrate the use of this proof system and to ...
    • Verifying Safety Properties Using Non-deterministic Infinite-state Automata 

      Klarlund, Nils; Schneider, Fred B. (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 ...
    • 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 ...