In this talk, we present an efficient static analysis based on Abstract Interpretation that aims at proving the absence of run-time errors in embedded multi-threaded C programs. Our method is based on a singe-thread analysis, enriched to infer and propagate abstract thread interferences. We prove that our method is sound with respect to a sequentially consistent semantics but also some weakly consistent memory models. We also show how partitioning techniques can model mutual exclusion and thread priorities. Finally, we present our prototype, AstréeA, based on the Astrée analyzer, as well as preliminary experimental results analyzing a large industrial program. AstréeA’s web site is at http://www.astreea.ens.fr/