Chalice is an experimental language that explores specification and verification of concurrency in programs. The language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. The language allows fine-grained locking via specifications that track fractional permissions for memory locations. The research project also includes an automatic static program verifier for Chalice.
Because of its permissions model, Chalice has also been used as a test bed for stepwise refinement. Using refinement, one can write an abstract program (call it pseudo-code) and then provide a more concrete implementation for that pseudo-code. The pseudo-code and its refinements all become part of the program text, and the Chalice verifier checks the correctness of the refinement steps. An episode of Verification Corner shows how this is done.
Chalice is available for download as open source from the Boogie open-source repository. There is also a nightly build that contains the binaries, available from “planned” releases on the Download tab.
If you want to program in Chalice or learn how its specifications are used (or, for that matter, to learn the basics of what makes a concurrent program correct), the Chalice tutorial is for you.