Enforcing high-level protocols in low-level software

By R. Deline, Manuel Fähndrich. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2001

486 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computer Networks and Communications, Hardware and Architecture

View Paper: https://www.semanticscholar.org/paper/34ea8ffd27f9bbb7fef494cfca41bed5f356be56

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Networks and Communications

In Hardware and Architecture

Citations in the corpus

The nesC language: A holistic approach to networked embedded systems (2003, methodology): “The static checking of software protocols in Vault [6] may provide an approach to solving these problems.”
Thorough static analysis of device drivers (2006, background): “Examples of such systems include the vault language [27] and the cqual type-system.”
Region-based memory management in cyclone (2002, methodology): “Two other recent projects, Vault [7] and the work of Henglein et al. [17] aim to provide safe source-level control over memory management using regions.”
Ownership, encapsulation and the disjointness of type and effect (2002, background): “Vault [25] extend C in a manner similar to Cyclone, though relying more on linearity instead of regions.”
Automatic predicate abstraction of C programs (2001, methodology): “Another approach is to use richer type systems to model nite-state abstractions of programs [14].”
Polyglot: An Extensible Compiler Framework for Java (2003, methodology): “To motivate our design, we show a simple extension of Java that supports some of the resource management facilities of the Vault language [7].”
Smallfoot: Modular Automatic Assertion Checking with Separation Logic (2005, unknown): “[13, 9]).”
Securing web application code by static analysis and runtime protection (2004, methodology): “[27] Foster, J. S., Fähndrich, M., Aiken, A.”
Automatically validating temporal safety properties of interfaces (2001, background): “An alternative approach to static validation of safety properties, is to provide a rich type system that allows users to encode both safety properties and program annotations as types, and reduce property validation to type checking [14].”
Bugs as deviant behavior: a general approach to inferring errors in systems code (2001, background): “While there has been some work on richer frameworks such as TypeState [23], Vault [6], and aspect-oriented programming [17], these still miss many systems relations and require programmer participation .”
Extended static checking for Java (2002, methodology): “A language in progress is Vault [7], whose promising ideas include using type-like features to take a next step in preventing certain kinds of resource-management programming errors.”
A type and effect system for atomicity (2003, background): “Vault [13] is a system designed to check resource management protocols, and lock-based synchronization can be considered to be such a protocol.”
The Spec# Programming System: An Overview (2004, background): “Similar effects have been achieved by ownership types and other alias-confinement strategies (e.g., [ 16 ,11]).”
ESP: path-sensitive program verification in polynomial time (2002, methodology): “In recent years, program analysis techniques have been used to build tools for partial verification [25, 11, 3, 10].”
Trusted Computing, Trusted Third Parties, and Verified Communications (2004, methodology): “With some research type systems (e.g., [ DeLine and Fahndrich, 2001; Myers, 1999]), the typing may ensure further properties, such as compliance with resource-usage rules and secure information-flow properties.”