More and more software systems, including in the critical industry,  exploit concurrency and multi-core architectures. Verifying concurrent  systems is challenging due to the huge number of possible executions  spawned by the (inherently highly non-deterministic) scheduler. Yet,  sound analyses covering all possible executions are necessary to  certify software and discover subtle concurrency bugs.
In this talk, we present several static analyses of such systems that  avoid considering explicitly all possible thread interleavings, and  use instead thread-modular techniques: we analyze separately each  thread as well as their interactions, performing a fixpoint to  propagate interactions between threads. The methods are based on  abstract interpretation, which ensures soundness by construction and  allows a wide range of cost versus precision trade-offs while  leveraging for free all the abstractions developed to analyze  sequential programs.
We present several analyses built on this model, including: an  extension to concurrent programs of the Astrée analyzer to prove the  absence of run-time errors in embedded critical C code, an analysis of  the functional correctness of device drivers in TinyOS, and an  analysis inferring numeric invariants in low-level concurrent programs  in the presence of weak hardware memory consistency models.