Title: Verification of concurrent programs with Chalice
Authors: Leino, K. Rustan M. * ×
Müller, Peter *
Smans, Jan * #
Issue Date: 10-Aug-2009
Publisher: Springer
Series Title: Lecture Notes in Computer Science vol:5705 pages:195-222
Conference: Foundations of Security Analysis and Design edition:5 date:30 August - 4 September 2009
Abstract: 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.
ISSN: 0302-9743
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
* (joint) first author
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
krml197.pdf Published 162KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.