Efficient implementations of abstract data types (ADTs) like collections (e.g., key-value stores, sets queues) and synchronization (e.g., signals, semaphores, locks) are essential to modern computing. Programming such objects is however error prone: in minimizing the synchronization overhead among concurrent invocations, one risks violating consistency with their ADTs. Developing automatic validation capable of mitigating such risks is also challenging. Compared to typical safety properties like assertion validity, which are easily verified in linear time per program execution, the runtime verification of consistency generally requires exponential time. Static consistency verification is generally undecidable without bounding the number of concurrent operations, whereas deciding assertion validity only requires bounding implementation state.

In recent works, we have developed scalable and effective methodologies for the specification and verification of concurrent objects. Exploiting the algebraic structure of common ADTs, we demonstrate improved theoretical limits for verification, effective approximations, and practical algorithms for inferring specifications and verifying implementations. Besides enabling tractable verification for many concurrent objects, our work has uncovered novel symbolic characterizations of consistency (e.g., linearizability) checking, which was previously thought to require explicit exponential enumeration (e.g., of possible linearizations).