Verifying Protocols in Concurrent Software Using Atomic Blocks and Alias Control

In object-oriented programs, it is often the case that object types define usage protocols as an implicit part of their interface. These protocols define legal orderings of method calls, and must be respected at run-time by code that uses objects of that type. Unfortunately, these protocols are implicit and are not checked as part of the compilation process. Statically verifying the correct usage of object protocols would b