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".