Formal Methods
Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
Ahmed Irfan
Publications | ahmed.irfan [at] unitn.it (Email)
More...
Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for transition systems represented in terms of SMT formulae. In this research we tackle the problems of SMT and VMT over the theories of nonlinear arithmetic over the reals (NRA) and of NRA augmented with transcendental (exponential and trigonometric) functions (NTA).
SMT-based formal verification of switched multi-domain Kirchhoff networks
Mirko Sessa
Publications | mirko.sessa [at] unitn.it (Email) | Website
More...
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
Publications | patrick.trentin [at] unitn.it (Email) | Website
More...
The last decades have witnessed techniques emerge as effective means for solving important industrial-level problems, mostly from Formal Verification. A recent extension of Satisfiability Modulo Theories (SMT) is Optimization Modulo Theories (OMT), which adds to SMT solvers the capability of optimizing objective functions. We plan to push forward OMT in terms of efficiency and expressiveness, and thus develop novel techniques for solving OMT problems. As part of our research, all extensions to OMT will be implemented on top of OPTIMATHSAT, our own OMT tool.
Effectively Encoding SAT and Other Intractable Problems into Ising Models for Quantum Computing
Stefano Varotti
Publications | stefano.varotti [at] unitn.it (Email)
More...
Quantum Annealers (QAs) are specialized Quantum Computers which efficiently find the minimum-energy configuration of a particular system by exploiting quantum effects.These QAs solve a restricted form of Quadratic Unconstrained Binary Optimization problems (QUBO). 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 my research is to investigate techniques and algorithms for encoding effectively and efficiently Propositional Satisfiability and other intractable problems forthe QA hardware architecture.