Research

Formal Methods for Systems and Software Design

The Formal Methods for Systems and Software Design (or simply FM) unit is part of the Digital Industry (DI) center at Fondazione Bruno Kessler (FBK). The activities of the FM unit focus on the research of novel and efficient formal methods for the verification, validation, and safety assurance of systems and software in various application domains including space, avionics, automotive, railways, energy, semiconductors, and manufacturing.

Topics of interest include:

• symbolic model checking
• satisfiability modulo theory (SMT)
• temporal logics
• compositional reasoning
• hybrid systems
• model-based safety analysis
• design of fault detection isolation and recovery (FDIR)
• monitoring, runtime verification, diagnosis and diagnosability

Our strategy is based on three pillars:

• high-quality research, publishing in top conferences such as CAV and TACAS as well as top journals such as Formal Methods in System Design, Formal Aspects of Computing, Information and Computation, and Artificial Intelligence - see our publications list
• well-known tools implementing various formal methods - see the list of tools including NuSMV, nuXmv, MathSAT, xSAP, OCRA, HyCOMP, and NuRV
• a variety of projects, where we apply and advance the techniques and tools to solve industrial problems in various application domains - see the list of current and past projects

If you are interested in our activities and want to collaborate, send an email to .

If you are fascinated by formal methods and would like to join our group, check out the current open calls or send us your cv at .