Arrival and Coffee: 9:30 - 10:00
Session 1: 10:00 - 10:45
Healfdene Goguen (AT&T Research)
A syntactic approach to eta equality in type theory
Break: 10:45 - 11:00
Session 2: 11:00 - 12:30
Eijiro Sumii (University of Pennsylvania)
Bisimulation for type abstraction and recursion
Pablo Garralda (Stevens Institute of Technology)
Boxed ambients with communication interfaces
Lunch: 12:30 - 1:50
Business meeting: 1:50 - 2:00
Session 3: 2:00 - 3:30
Radu Rugina (Cornell University)
Shape analysis with local reasoning
Rustan Leino (Microsoft Research)
The Spec# programming system
Abstract: We present a sound, complete, and elementary proof method---based on bisimulation---for contextual equivalence in lambda-calculus with full universal, existential, and recursive types. Unlike logical relations (either semantic or syntactic), our development is elementary, using only sets and relations and avoiding advanced machinery such as domain theory, admissibility, and TT-closure. Unlike other bisimulations, ours is complete even for existential types. The key idea is to consider _sets_ of relations---instead of just relations---as bisimulations.
Abstract: BACI (Boxed Ambients with Communication Interfaces) is an ambient calculus based on Boxed Ambients, and it is a calculus that allows a liberal communication policy. Each ambient carries its local view of the topic of conversation (the type of the information being exchanged) with parents and children ambients. The local view conditions the mobility of an ambient and the mobility of other ambients attempting to enter it. This local view has partial knowledge of the topic of conversation with each possible parent and child ambient. This view can also be dynamically augmented during migration. BACI is flexible enough to allow different topics of conversation between an ambient and different parents, without compromising type-safety: it uses port names for communication and ambient names for mobility. Capabilities and co-capabilities exchange port names and run-time typing information to control mobility. We show the type-soundness of BACI proving that it satisfies the subject reduction property. Moreover we study its behavioral semantics by means of a labeled transition system.
Joint work with Eduardo Bonelli, Adriana Compagnoni, and Mariangiola Dezani-Ciancaglini.
Abstract: Shape analyses are static analyses aimed at extracting invariants that describe the "shapes" of dynamically allocated recursive structures. Although existing shape analyses have been successful at verifying complex heap manipulations, they have had limited success at being practical for larger programs.
In this talk I will present a novel approach to shape analysis that uses local reasoning about individual heap locations instead of global reasoning about entire heap abstractions. The key feature of this approach is a novel memory abstraction that models the heap using a set of independent configurations, each of which characterizes one single heap location. This approach: 1) leads to simpler algorithm specifications, because of local reasoning about the single location; 2) leads to efficient algorithms, because of the finer abstraction granularity; and 3) makes it easier to develop context-sensitive, demand-driven, and incremental shape analyses.
I will also present a prototype system that uses shape analysis to detect memory leaks and accesses through dangling pointers in C programs. The current results suggest that the local reasoning approach is sufficiently lightweight to scale to larger programs, and sufficiently accurate to detect errors with low false positive rates.
Abstract: The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. Central to the programming system is the Spec# programming language, an experimental superset of the language C#, including non-null types, pre- and postconditions, and object invariants. Spec# attempts to raise the bar in helping programmers manage program details by: checking the enriched types in the compiler, emitting dynamic checks for contracts, and offering static program verification with the tool Boogie.
This talk describes the Spec# programming system, focusing on some difficult issues in its design. The talk also includes a short demo of Spec# and Boogie.