- Homepage
- About the Joint Centre
- Research Areas & Projects
- Researchers
- News & Events
- Open Positions
Friday, January 16, 2009, 11h, bdg I, 1st floor,
the MSR-INRIA Joint Centre,
Inria Saclay,
Correct Concurrency with Chalice,
Rustan Leino,
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.