We study the automatic verification of asynchronous message-passing concurrent programs. This talk will begin with a survey of a recent project [1], Soter, to verify safety properties of Erlang programs by abstract interpretation and infinite-state model checking, and a discussion of the lessons learn. The rest of the talk will focus on an approach to address a source of imprecision of the Soter approach. We study the reachability problem of concurrent pushdown systems that communicate via unbounded and unordered message buffers, a model of computation for Erlang programs. Our goal is to relax the common restriction that messages can only be retrieved by a pushdown process when its stack is empty. We introduce a new class of Asynchronously Partially Commutative Pushdown Systems with a mild shape constraint on the stacks for which the coverability problem is decidable. Stacks that fit the shape constraint may reach arbitrary heights; further a process may execute any communication action (be it process creation, message send or retrieval) whether or not its stack is empty. This class extends previous computational models studied in the setting of asynchronous procedural calls, and enables the safety verification of a large class of recursively-defined message-passing programs. This is joint work with Jonathan Kochems and Emanuele D'Osualdo. [1] [1]http://mjolnir.cs.ox.ac.uk/soter