Sciweavers

FOSAD
2009
Springer

Verification of Concurrent Programs with Chalice

14 years 3 months ago
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.
K. Rustan M. Leino, Peter Müller, Jan Smans
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2009
Where FOSAD
Authors K. Rustan M. Leino, Peter Müller, Jan Smans
Comments (0)