Computing Publications

Publications Home » A Sip of the Chalice

A Sip of the Chalice

Azalea Raad

Conference or Workshop Paper
FTfJP 2011
July, 2011
ACM Digital Library
ACM Press
Abstract

Chalice is a veri cation tool for object-based concurrent programs. It supports veri cation of functional properties of the programs as well as providing a deadlock prevention mechanism. It is built on Implicit Dynamic Frames, fractional permissions and permission transfer.

Implicit Dynamic Frames have been formulated and proven sound using veri cation conditions and axiomatisation of the heap and stack. Veri cation in Chalice is specified in terms of weakest preconditions and havocing the heap.

In this paper we give a formalisation of the part of Chalice concerned with functional properties. We describe its operational semantics, Hoare logic and sketch the soundness proof. Our system is parametric with respect to the underlying assertion language.

Keywords
Concurrency
Program Verification
SLURP
PDF of full publication (429 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.