Verification of Concurrent Programs with Chalice

A program verifier is a tool that allows developers to prove that their code satisfies its specification for every possible input and every thread schedule. These lecture notes describe a verifier for concurrent programs called Chalice. Chalice's verification methodology centers around permissions and permission transfer. In particular, a memory location may be accessed by a thread only if that thread has permission to do so. Proper use of permissions allows Chalice to deduce upper bounds on the set of locations modifiable by a method and guarantees the absence of data races for concurrent programs. The lecture notes informally explain how Chalice works through various examples.

• Type: Conference
• Year: 2009
• Where: FOSAD
• Authors: K. Rustan M. Leino, Peter Müller, Jan Smans
• Keywords: Chalice's Verification Methodology, Concurrent Programs, FOSAD 2009, Programs Called Chalice, Security Privacy