About Chalice - A language and program verifier for reasoning about concurrent programs.
Chalice is a simple imperative programming language with constructs for thread creation, locking, and channels. The language has built-in specification constructs, and specifications are written in the style of implicit dynamic frames with fractional permissions.