Multiprocessor machines are now predominant, as most laptops, desktops, servers, mobile phones and aircrafts routinely have multiple to many cores. Unfortunately, concurrent programming is error-prone, which now affects everyone given this trend towards more and more concurrency. Let us mention for example a recent concurrency bug found in the PostgreSQL database (see http://archives.postgresql.org/pgsql-hackers/2011-08/msg00330.php). PostgreSQL is one of the most popular database nowadays, and many websites rely on its correct functioning. This bug was particularly difficult to observe (and indeed is not fixed yet) because it only occurred on a multicore machine, and a particular hardware platform, IBM Power. Reproducing such bugs is as hard as observing them; thus testing can hardly discover them. To prove a program free of errors, we would like to devise automated techniques that analyse the code without executing it. Thus, we can relieve programmers from the burden of writing the proofs of their programs. Yet, automatic verification of concurrent programs represents a challenge, whether it aims at proving the full correctness of a program (e.g. a program sorting a list actually sorts the list), or at checking specific properties (e.g. the program is free of data races) short of full correctness. We focus here on the latter: we would like to enhance the scalability of tools checking that a concurrent program does not violate certain safety-critical properties of interest. We would like to show that scalable automatic verification can be achieved by exploiting the rich history of partial orders for modeling concurrency.