In this talk we discuss formal verification of the C# joins library,
which provides a declarative way of defining synchronization
primitives.  The joins library provides an excellent challenge for
verification, as it combines state, fine-grained concurrency and
recursion through the store in a realistic and reasonably small
library.

We present a specification for the joins library that allows clients
to reason in terms of high-level joins primitives, and discuss
challenges in verifying the implementation.  We present a higher-order
variant of concurrent abstract predicates with support for
state-independent higher-order protocols.