

Failure Propagation, Diagnosability, and Recoverability Analysis for safetycritical systems
Benjamin Bittner
Formal Methods, FDIR, Failure Propagation, Diagnosis, Recovery
In order to successfully implement failure management functions in safetycritical 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.
Publications



SMTbased Formal Verification of NonLinear Transition Systems
Linearization Techniques
Ahmed Irfan
smt, formal verification, nonlinear, transition systems, model checking, linearization
Model checking of designs, represented as transition systems, with nonlinear real arithmetic (NRA), is an important though very hard problem. On the one hand NRA is a hardtosolve 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).
Publications



Formal verification of hybrid multidomain 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 MultiDomain 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 SMTbased techniques whose main benefit is to analyze sets of configurations at once, hence scaling to industrial size networks.
Website
Publications



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 industriallevel 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.
Publications



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 minimumenergy configuration of a particular system by exploiting quantum effects. Since 2007 DWave (www.dwavesys.com) has been building QAs with a Moorelike 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 seconddegree polynomial over binary variables. QAs provide verypromising tools for solving NPHard problems. Although DWave’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 DWave, 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.
Publications
