Friday, January 16, 2009, 11h, bdg I, 1st floor,
the MSR-INRIA Joint Centre,
Correct Concurrency with Chalice,
Microsoft Research, Redmond,
Chalice is an experimental language for writing and verifying concurrent programs using shared memory and mutual exclusion via locks. The semantic model for the language uses fractional permissions that can be divided up between and transferred among threads–more precisely, their method invocations and loop iterations–and monitors. The semantics is translated into first-order verification conditions, which are discharged by an SMT solver. In this talk, I will describe the language, its semantics, and its static verifier.