Modern software developments kits simplify the programming of concurrent or distributed applications by providing shared state abstractions which encapsulate low-level accesses into higher-level abstract data types (ADTs). Programming such abstractions is however error prone. To minimize synchronization overhead between concurrent ADT invocations, implementors avoid blocking operations like lock acquisition, allowing methods to execute concurrently. However, concurrency risks unintended inter-operation interference, and risks conformance to well-established correctness criteria like linearizability or causal consistency. We present a generic proof methodology for verifying such ADTs based on forward simulations.