Techniques based on formal methods for the verification and validation of embedded and safety-critical 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 remains a challenge in practice, due to factors such as poor
scalability, lack of automation, the interplay between computation and physical aspects, or 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
systems, with particular emphasis on safety-critical application domains such as railways, automotive, avionics, and aerospace. A particular
attention will be devoted to improving the scalability and degree of automation of formal methods techniques, with a specific focus on
symbolic model checking methods using satisfiability and satisfiability modulo theories solvers as symbolic reasoning engines. 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.