Mainstream programming languages offer libraries of concurrent data structures. Each method call on a concurrent data structure appears to take effect atomically. However, clients of such data structures often require stronger guarantees. We have developed an automatic and modular verification technique for clients of concurrent data structures along with a novel sufficient condition for atomicity of clients called condensability and constructed a tool called Snowflake that generates proof obligations for condensability of Java client methods.