To improve performance, virtually all modern processors (e.g. Power, SPARC, Intel, ARM) support relaxed memory models. Unfortunately, programming these relaxed models is difficult and error-prone, yet highly desirable. In this project, we develop powerful automated synthesis and verification techniques which ensure that modern chips are exploited correctly and efficiently. The techniques are based on model checking, abstract interpretation and dynamic analysis.