Now showing items 40-59 of 101

• #### Faster Possibility Detection by Combining Two Approaches ﻿

(Cornell University, 1995-04)
A new algorithm is presented for detecting whether a particular computation of an asynchronous distributed system satisfies $\Poss\Phi$ (read "possibly $\Phi$"), meaning the system could have passed through a global state ...

(Cornell University, 1983-09)
A distributed program is presented that ensures delivery of a message to the functioning processors in a computer network, despite the fact that processors may fail at any time. All processor failures are assumedd to be ...
• #### Federated Identity Management Systems: A Privacy-based Characterization ﻿

(2012-10-16)
Identity management systems store attributes associated with users and facilitate authorization on the basis of these attributes. A privacy-driven characterization of the principal design choices for identity management ...
• #### Fine-Grained User Privacy from Avenance Tags ﻿

(2014-04-20)
In the Internet, users interact with service providers; these interactions exchange information that might be considered private by the user. Existing schemes for expressing and enforcing user privacy on the Internet---notably ...
• #### Formalizations Of Substitution Of Equals For Equals ﻿

(Cornell University, 1998-05)
Inference rule "substitution of equals for equals" has been formalized in terms of simple substitution (which performs a replacement even though a free occurrence of a variable is captured), contextual substitution (which ...
• #### 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 ...