Techniques based on formal methods for the verification and validation of embedded and safety-critical software systems are becoming increasingly important, due to the growing complexity and importance of such systems in every aspect of modern society. Despite the major progress seen in the last twenty years, however, the application of formal methods in embedded software remains a challenge in practice, due to factors such as the interplay between computation and physical aspects and the increasing complexity of the software and its configurations. This project will investigate novel techniques for the application of formal methods to the design, verification, and validation of embedded software, with particular emphasis on safety-critical application domains such as railways, automotive, avionics, and aerospace. The techniques considered will include a combination of automated and interactive theorem proving, satisfiability modulo theories, model checking, abstract interpretation, and deductive verification. Examples of the problems tackled during the project include the formal verification of functional requirements expressed in temporal logics, automated test-case generation, efficient handling of parametric/multi-configuration software systems and product lines, and the verification of software operating in a physical environment, subject to real-time constraints. Importantly, in addition to researching novel theoretical results, a significant part of the project activities will be devoted to the implementation of the techniques in state-of-the-art verification tools developed at FBK and their application to real-world problems in collaboration with our industrial partners.