PhD positions in collaboration with the University of Trento on formal-methods-related topics
Apr 16, 2025
Three PhD positions are available at FBK, in collaboration with the University of Trento. The deadline for application is May 12th.
C3 - Certifying model checking (1 grant)
Abstract: In the field of formal verification, certifying proofs serve as compelling evidence to demonstrate the correctness of a model within a deductive system. These proofs can be automatically generated as a by-product of the verification process and are key artifacts for high-assurance systems. Their significance lies in their ability to be independently verified by proof checkers, which provides a more convenient approach than certifying the tools that generate them. Model checking is one of the leading formal techniques used in the domain of hardware verification and synthesis, and it relies on an algorithmic exploration of the system's state space to ensure that the system behaves as expected over time. Modern model checking tools are sophisticated pieces of software, employing a wide range of diverse techniques to increase their performance, effectiveness, and scalability to real-world problem instances. Although often their underlying algorithms are capable of producing some form of proof, ensuring that such core proofs are compatible with the transformation and optimization techniques applied to the input system remains a challenge. The objective of this project is that of developing novel techniques for the reconstruction of proofs in model checking, so as to be able to certify their results. We will consider different proof formalisms and certification strategies, leveraging both interactive theorem provers and automatic decision procedures based on propositional satisfiability (SAT) and satisfiability modulo theories (SMT). The candidate is expected to explore not only explore theoretical results, but also practical implementations on state-of-the-art model checking tools developed at FBK, and their applications to real-world problems.
Contact: Alberto Griggio griggio@fbk.eu
C4 - Failure analysis and safety assessment of complex industrial systems (1 grant)
Abstract: Industrial systems are reaching an unprecedented degree of complexity. The design process has to guarantee not only the functional correctness of the implemented system, but also its dependability and resilience with respect to run-time faults. Hence, the design process must characterize the likelihood of faults, mitigate possible failures, and assess the effectiveness of the adopted mitigation measures.
Formal methods have been increasingly used over the last decades to deal with the shortcomings of designing complex systems, in different domains. Formal methods are based on the adoption of a formal, mathematical model of the system, shared between all actors involved in the system design, and on a tool-supported methodology to aid all the steps of the design, from the definition of the architecture down to the final implementation in HW and SW. Formal methods include technologies such as model checking, an automatic technique to symbolically and exhaustively analyze all possible executions of the system in the formal model, in order to detect design flaws as early as possible. Model checking techniques have been recently extended to assess the safety and dependability characteristics of the design, and for system certification.
The objective of this study is to advance the state-of-the-art in failure analysis and safety assessment of complex industrial systems. In particular, it will investigate extensions of existing fault propagation models and failure analysis techniques to deal with aspects such as the timing of fault propagation, the impact on system degradation, the characterization of transient and sporadic faults, and the analysis of the effectiveness of fault mitigation measures in presence of complex fault patterns. Moreover, this study will address the formal design of fault detection, isolation, and recovery (FDIR) sub-systems, techniques for diagnosis and root-cause analysis using formal methods, anomaly detection and FDIR based on machine learning techniques.
The developed techniques will be implemented and evaluated using tools for system-software engineering such as the COMPASS and the TASTE tools. This study is aligned with the topics investigated in various industrial projects carried out at FBK, such as the COMPASTA and AIFDIR projects, funded by the European and Italian Space Agencies.
Contact: Marco Bozzano bozzano@fbk.eu
C5 - SMT-based software model checking (1 grant)
Abstract: Techniques based on formal methods for the verification and validation of 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 and various examples of success stories, however, the application of formal methods, and especially automatic or fully-automatic techniques, in software remains a challenge in practice. This project will investigate novel techniques for the application of formal methods to the design, verification, and validation of software, with particular emphasis on safety-critical application domains such as railways, automotive, avionics, and aerospace. The primary focus will be on automatic techniques combining model checking and automated theorem proving based on the Satisfiability Modulo Theories (SMT) paradigm, but other related techniques such as interactive theorem proving, abstract interpretation, or deductive verification will be considered as well. 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.
Contact: Alberto Griggio griggio@fbk.eu