Failure Propagation, Diagnosability, and Recoverability Analysis for safety-critical systems

Benjamin Bittner

Formal Methods, FDIR, Failure Propagation, Diagnosis, Recovery

In order to successfully implement failure management functions in safety-critical systems, corresponding formal failure propagation analysis methods and adequate V&V methods for the designs are fundamental. We propose a framework based on formal methods for timed failure propagation analysis, diagnosability analysis, and recoverability analysis, to be applied to design models of the system at hand.




SMT-based Formal Verification of Non-Linear Transition Systems

Linearization Techniques

Ahmed Irfan

smt, formal verification, non-linear, transition systems, model checking, linearization

Model checking of designs, represented as transition systems, with non-linear real arithmetic (NRA), is an important though very hard problem. On the one hand NRA is a hard-to-solve theory; on the other hand most of the powerful model checking techniques lack support for NRA. In this research, we work on linearization techniques to enable the use of mature and efficient model checking algorithms for transition systems on linear real arithmetic (LRA) with uninterpreted functions (EUF).




Formal verification of hybrid multi-domain conservative flow networks

Mirko Sessa

formal methods, hybrid systems, safety verification, acausal modeling

Many critical systems are based on the combination of components from different physical domains (e.g. mechanical, electrical, hydraulic) and are mathematically modeled as Switched Multi-Domain Kirchhoff Networks (SMDKN). Our research tackles a major obstacle to formal verification of SMDKN, namely devising a global model amenable to verification in the form of a Hybrid Automaton. Since SMDKN exhibit exponentially many global configurations, we apply SMT-based techniques whose main benefit is to analyze sets of configurations at once, hence scaling to industrial size networks.





Broadening the Horizon of Optimization Modulo Theories

Patrick Trentin

optimization modulo theory, omt, satisfiability modulo theory, constraint programming, maxsmt, satisfiability, optimization

The last decades have witnessed Satisfiability Modulo Theories (SMT) techniques emerge as effective means for solving important industrial-level problems, mostly from Formal Verification. A recent extension of SMT is Optimization Modulo Theories (OMT), which adds to SMT solvers the capability of optimizing objective functions. To date, few OMT solvers exist, and the OMT technol- ogy is still at an early stage. The goal of this research is twofold. First, we plan to push forward OMT in terms of efficiency and expressiveness, and thus develop novel techniques for solving OMT problems. Second, we plan to investigate the effectiveness of OMT beyond the Formal Verification scope, and study its effectiveness in dealing with problems traditionally solved with Constrained Programming (CP) and Mixed Integer Linear Programming (MILP). As part of our research, all extensions to OMT will be implemented on top of O PTIMATHSAT, our own OMT tool.




Effectively Encoding SAT and Other Intractable Problems into Ising Models for Quantum Computing

Stefano Varotti

Satisfiability, SAT, Quantum Annealing, QUBO

Quantum Annealers (QAs) are specialized Quantum Computers which efficiently find the minimum-energy configuration of a particular system by exploiting quantum effects. Since 2007 D-Wave ( has been building QAs with a Moore-like growth rate, reaching the current ∼2000qbit architecture. These QAs solve a restricted form of Quadratic Unconstrained Binary Optimization problems (QUBO), aka Ising model, consisting in finding the minimum value of a second-degree polynomial over binary variables. QAs provide very-promising tools for solving NP-Hard problems. Although D-Wave’s QAs outperform standard computers on random QUBO problems, it is not yet possible to obtain benefits for many other problem classes. The goal of this research proposal, which is held in collaboration with D-Wave, is to investigate techniques and algorithms for encoding effectively and efficiently Propositional Satisfiability and other intractable problems into the restricted class of QUBOs that fit the QA hardware architecture, s.t. to exploit the computing power of QAs.