Refinement types enrich a language's type system with logical predicates that circumscribe
the set of values described by the type. These refinement predicates provide software …

In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have
developed an extension of Hoare logic that permits reasoning about low-level imperative …

Given the central role that C continues to play in systems software, and the difficulty of
writing safe and correct C code, it remains a grand challenge to develop effective formal …

Reynolds has developed a logic for reasoning about mutable data structures in which the
pre-and postconditions are written in an intuitionistic logic enriched with a spatial form of …

During the past twenty-one years, over seventy-five papers and nine Ph. D. theses have
been published on pointer analysis. Given the tomes of work on this topic one may …

We describe a type system for checking interference using the concept of linear capabilities
(which we call “permissions”). Our innovations include the concept of “fractional” …

Separation logic is a program logic for reasoning about programs that manipulate pointer
data structures. We describe Smallfoot, a tool for checking certain lightweight separation …

We describe a sound method for automatically proving Hoare triples for loop-free code in
Separation Logic, for certain preconditions and postconditions (symbolic heaps). The …

Noninterference is a property of sequential programs that is useful for expressing security
policies for data confidentiality and integrity. However, extending noninterference to …

We present a system for extending standard type systems with flow-sensitive type qualifiers.
Users annotate their programs with type qualifiers, and inference checks that the …