Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to their abstract data types (ADTs) — or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable. Existing approaches are thus either limited to executions with very few object invocations, or rely on programmer interaction.

We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violation-detection algorithms. Furthermore, our approach does not require programmer interaction, for instance, in identifying linearization points. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions.