Leino, K. Rustan M. * × Müller, Peter * Smans, Jan * #
Lecture Notes in Computer Science vol:5705 pages:195-222
Foundations of Security Analysis and Design edition:5 date:30 August - 4 September 2009
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.