A sip of the Chalice
Azalea Raad, Sophia Drossopoulou · 2011
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.