SBMF 2010 INVITED TALKS

Dynamic Boundaries: Global Invariants for Local Reasoning

By David Naumann

The hiding of internal invariants creates a mismatch between procedure specifications in an interface and proof obligations on the implementations of those procedures. The mismatch is sound if the invariants depend only on encapsulated state, but encapsulation is problematic in contemporary software due to the many uses of shared mutable objects. In this talk I propose a new interface specification feature, the dynamic boundary, which achieves flexibility via explicit restrictions on client effects, expressed using ghost state and ordinary first order assertions.

Joint work with Stan Rosenberg and Anindya Banerjee



SVA: Using CSP to Analyse Shared Variable Programs

By Bill Roscoe

SVA is a new tool developed by me and David Hopkins that translates ashared variable program into CSP and analyses it on FDR. I will discuss how this translation is done, the great effectiveness of FDR's compression functions on the result and a model of refinement between shared variable program fragments. As examples I will solve an open problem regarding Simpson's 4-slot algorithm and show how a finite model checking run can prove the bakery algorithm for an unbounded ticket type and an arbitrary number of nodes.

This talk is based on Chapters 18 and 19 of my forthcoming book "Understanding Concurrent Systems".