We offer a language for specifying the abstraction (model) that a Java class
implements. Given specifications of conditions under which operations conflict,
we can prove those specifications correct, and possibly derive them. We can
also prove correctness of inverse (compensating) actions at the abstract level.
All this is possible because the model language is carefully designed to be powerful enough to specify interesting abstractions yet restricted enough to allow automated proofs of correctness. We briefly describe Set and OrderedSet abstractions and mention results of automated proofs to date. This technology overcomes the criticism of open nesting that abstract concurrency control is too difficult for programmers to get right.

The Other.pdf document is Trek Palmer's PhD proposal on this work.