Now showing items 45-64 of 101

• #### A Graphical Interface for CHIP ﻿

(Cornell University, 1996-06)
CHIP (Cornell Hypothetical Instructional Processor) [BBDS83] is a computer system designed as an educational tool for teaching undergraduate courses in operating system and machine architecture. This document describes ...
• #### The "Hoare Logic" of CSP, and All That ﻿

(Cornell University, 1982-05)
Generalized Hoare Logic is a formal logical system for deriving invariance properties of programs. It provides a uniform way to describe a variety of methods for reasoning about concurrent programs, including noninterference, ...
• #### The HOCA Operating System Specifications ﻿

(Cornell University, 1983-12)
NO ABSTRACT SUPPLIED
• #### Hybrid Verification by Exploiting the Environment ﻿

(Cornell University, 1994-07)
A method of verifying hybrid systems is given. Such systems involve state components whose values are changed by continuous (physical) processes. The verification method is based on proving that only those executions ...
• #### Hyperproperties ﻿

(2008-01-27)
Properties, which have long been used for reasoning about systems, are sets of traces. Hyperproperties, introduced here, are sets of properties. Hyperproperties can express security policies, such as secure information ...
• #### Hyperproperties ﻿

(2008-12-22)
Properties, which have long been used for reasoning about systems, are sets of traces. Hyperproperties, introduced here, are sets of properties. Hyperproperties can express security policies, such as secure information ...
• #### Hypervisor-based Fault-tolerance ﻿

(Cornell University, 1995-03)
Protocols to implement a fault-tolerant computing system are described. These protocols augment the hypervisor of a virtual machine manager to coordinate a primary virtual machine and its backup. The result is a ...
• #### Independence From Obfuscation: A Semantic Framework for Diversity ﻿

(Cornell University, 2006-01-30)
A set of replicas is diverse to the extent that all implement the same functionality but differ in their implementation details. Diverse replicas are less prone to having vulnerabilities in common, because attacks typically ...
• #### Inexact Agreement: Accuracy, Precision, and Graceful Degradation ﻿

(Cornell University, 1985-05)
An Inexact Agreement protocol alows processors that each have a value approximating $\hat{\nu}$ to compute new values that are closer to each other and close to $\hat{\nu}$. Two fault-tolerant protocols for Inexact ...
• #### JRIF: Reactive Information Flow Control for Java ﻿

(2016-02-12)
A reactive information flow (RIF) automaton for a value v specifies (i) allowed uses for v and (ii) the RIF automaton for any value that might be directly or indirectly derived from v. RIF automata thus specify how ...
• #### Key Exchange Using Keyless Cryptography ﻿

(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 ...
• #### Mechanisms for Specifying Scheduling Policies ﻿

(Cornell University, 1979-02)
Extensions to concurrent programming languages are presented which allow control of scheduling policies previously defined by the run-time support system. It is shown that the use of these mechanisms simplifies the ...
• #### Multi-Verifier Signatures ﻿

(2009-08-15)
Multi-verifier signatures generalize traditional digital signatures to a secret-key setting. Just like digital signatures, these signatures are both transferable and secure under arbitrary (unbounded) adaptive chosen-message ...
• #### NAP: Practical Fault-Tolerance for Itinerant Computations ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ﻿

(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 ﻿

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