The Action coordinates the development of infrastructures for automated reasoning about Rich Models of computer systems. Rich Models have the expressive power of all practically formalizable mathematics, enabling natural specification of software, hardware, embedded, and distributed systems. Rich Models support modeling at a wide range of abstraction levels, from knowledge bases and system architecture, to software source code and detailed hardware design. The Action contributes to the construction of a Rich Model Toolkit, which is a unified infrastructure that precisely defines the meaning of Rich Models, standardizes representation formats, and supports a number of automated reasoning tools. Moreover, the Action develops and deploys new tools for automated reasoning that communicate using these standardized formats. The goal of resulting tools is to have a wide range of applicability and improved efficiency, helping system developers construct reliable systems through automated reasoning, analysis, and synthesis. The funds of the Action are handled by EPFL (Ecole Polytechnique Fédérale de Lausanne, Laboratoire LARA) from 30/10/2009 through 31/12/2010 and by IMDEA (Universidad Politécnica de Madrid, Facultad de Informática, Fundación IMDEA Software) from 1/1/2011 onwards.