research-article

A sip of the Chalice

Authors:

Azalea Raad,

Sophia DrossopoulouAuthors Info & Claims

FTfJP '11: Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs

Article No.: 2, Pages 1 - 30

https://doi.org/10.1145/2076674.2076676

Published: 25 July 2011 Publication History

Get Access

Abstract

Chalice is a verification tool for object-based concurrent programs. It supports verification 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 verification conditions and axiomatisation of the heap and stack. Verification 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.

References

[1]

Nick Benton, Luca Cardelli, and Cedric Fournet. Modern concurrency abstractions for c#. TOPLAS, 2004.

Digital Library

Google Scholar

[2]

John Boyland. Checking interference with fractional permissions. In Static Analysis: 10th International Symposium, pages 55--72. Springer, 2003.

Digital Library

Google Scholar

[3]

Christian Haack and Clément Hurlin. Separation logic contracts for a Java-like language with fork/join. In International Conference on Algebraic Methodology and Software Technology (AMAST'08), July 2008.

Digital Library

Google Scholar

[4]

Clément Hurlin. Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic. PhD thesis, Université Nice - Sophia Antipolis, September 2009.

Google Scholar

[5]

K. Rustan Leino and Peter Müller. A basis for verifying multi-threaded programs. In Proceedings of the 18th European Symposium on Programming Languages and Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, ESOP '09, pages 378--393, Berlin, Heidelberg, 2009. Springer-Verlag.

Digital Library

Google Scholar

[6]

K. Rustan Leino, Peter Müller, and Jan Smans. Verification of Concurrent Programs with Chalice, pages 195--222. Springer-Verlag, Berlin, Heidelberg, 2009.

Digital Library

Google Scholar

[7]

M. J. Parkinson and A. J. Summers. The relationship between separation logic and implicit dynamic frames. In Gilles Barthe, editor, European Symposium on Programming (ESOP), volume 6602 of Lecture Notes in Computer Science. Springer-Verlag, 2011.

Digital Library

Google Scholar

[8]

Jan Smans, Bart Jacobs, and Frank Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In Proceedings of the 23rd European Conference on ECOOP 2009 --- Object-Oriented Programming, Genoa, pages 148--172, Berlin, Heidelberg, 2009. Springer-Verlag.

Digital Library

Google Scholar

Cited By

View all

Drossopoulou SNoble JDietl W(2013)The need for capability policiesProceedings of the 15th Workshop on Formal Techniques for Java-like Programs10.1145/2489804.2489811(1-7)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1145/2489804.2489811
Summers ADrossopoulou S(2013)A formal semantics for isorecursive and equirecursive state abstractionsProceedings of the 27th European conference on Object-Oriented Programming10.1007/978-3-642-39038-8_6(129-153)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-39038-8_6

Index Terms

A sip of the Chalice

Recommendations

Verifying concurrent programs with chalice
VMCAI'10: Proceedings of the 11th international conference on Verification, Model Checking, and Abstract Interpretation

One of the problems in verifying concurrent programs is keeping track of which threads have access to which data at which times. The experimental language Chalice makes this explicit by requiring every data access to be justified with a sufficient set ...
Verification of Concurrent Programs with Chalice
Foundations of Security Analysis and Design V

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 ...
Stepwise refinement of heap-manipulating code in Chalice
Abstract
Stepwise refinement is a well-studied technique for developing a program from an abstract description to a concrete implementation. This paper describes a system with automated tool support for refinement, powered by a state-of-the-art ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

FTfJP '11: Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs

July 2011

85 pages

ISBN:9781450308939

DOI:10.1145/2076674

Conference Chair:
Stephen Freund
Williams College

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 July 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

ECOOP '11

Sponsor:

Lancaster University
AITO

ECOOP '11: European Conference on Object-Oriented Programming

July 25 - 29, 2011

Lancaster, United Kingdom

Acceptance Rates

Overall Acceptance Rate 51 of 75 submissions, 68%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
66
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Drossopoulou SNoble JDietl W(2013)The need for capability policiesProceedings of the 15th Workshop on Formal Techniques for Java-like Programs10.1145/2489804.2489811(1-7)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1145/2489804.2489811
Summers ADrossopoulou S(2013)A formal semantics for isorecursive and equirecursive state abstractionsProceedings of the 27th European conference on Object-Oriented Programming10.1007/978-3-642-39038-8_6(129-153)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-39038-8_6

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Verifying concurrent programs with chalice

Verification of Concurrent Programs with Chalice

Stepwise refinement of heap-manipulating code in Chalice