Verification of concurrent programs with Chalice

K. Rustan M. Leino, Peter Müller, Jan Smans
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 15 February 2020

Foundations of Security Analysis and Design V: FOSAD 2007/2008/2009 Tutorial Lectures
Springer Berlin Heidelberg
Berlin, Heidelberg
Pages 195-222
2009
Topic(s): tools verification
Note(s): permission logic, modular verification, contract driven development, fractional permissions, permission accounting, Chalice verifier, ghost code

This is a tutorial on the Chalice object-oriented language and verifier. Methods have contracts, loops have invariants, pointers have ownership annotations, there are threads, locks and fractional ownership, there are lock orderings to detect deadlock and there are ghost variables and fold/unfold ghost statements.

The language seems to have had more attention paid to usability than normal.

  • For example, fractional permissions get the job done – but they are a slightly obscure way to say that something is “read only” so Chalice has notation to say that something is read only.

  • There are command line options to reduce the amount of annotation required:

    • unfolding and folding predicates at the start/end of each method

    • automatically trying to fold when a predicate is required

The conclusions section is great: it explains the influences, where ideas came from, who did what and where the reader might find more about the concepts in this language/tool.

  • Viper: A verification infrastructure for permission-based reasoning [muller:vmcai:2016]