enter search term and/or author name
On loops, dominators, and dominance frontiers
This article explores the concept of loops and loop nesting forests of control-flow graphs, using the problem of constructing the dominator tree of a graph and the problem of computing the iterated dominance frontier of a set of vertices in a graph...
Data abstraction and information hiding
K. Rustan M. Leino, Greg Nelson
This article describes an approach for verifying programs in the presence of data abstraction and information hiding, which are key features of modern programming languages with objects and modules. This article draws on our experience building and...
The undecidability of associativity and commutativity analysis
Associativity is required for the use of general scans and reductions in parallel languages. Some systems also require functions used with scans and reductions to be commutative. We prove the undecidability of both associativity and commutativity....
Information flow vs. resource access in the asynchronous pi-calculus
Matthew Hennessy, James Riely
We propose an extension of the asynchronous π-calculus in which a variety of security properties may be captured using types. These are an extension of the input/output types for the π-calculus in which I/O capabilities are assigned specific...