Roberto Sebastiani - Research Interests

• Satisfiability Modulo Theories (SMT) and its applications.
  SMT is the problem of checking satisfiability of formulas in complex theories which extend boolean satisfiability (typically decidable subclasses of First-order logic). SMT tools are nowadays widely used in industries as horsepower reasoning engines, in particular in the verification of both SW and HW systems. I'm one one of the inventors of the “lazy” approach to SMT (now implemented in most state-of-the-art SMT tools), which combines SAT solvers with decision procedures for the conjunctive fragment of the theories. Since 2002 I've been giving essential contributions, from both theoretical and empirical viewpoint, in SMT solving and in advanced SMT techniques, like theory combination, interpolation, unsatisfiable-core extraction. All these techniques have been implemented into the state-of-the-art SMT tool MathSAT.
• Optimization Modulo Theories (OMT) and its applications.
  Since 2012 I have initiated and have been pushing forward the field of Optimization Modulo Theories (OMT) as a very-useful extension of SMT –and viable alternative to MILP and Constraint Programming– in many application domains. All the OMT techniques developed have been implemented into the state-of-the-art OMT tool OptiMathSAT.
• Formal Verification, Model Checking.
  My main research contributions in formal verifications are divided into two main streams.
  • First, I have contributed to the research on model checking (MC), by investigating novel LTL model checking algorithms, both theoretically and empirically.
    
  • Second, I'm one of the main contributors of SMT-based model checking, which leverages previous SAT-based MC to much more expressive application domains –e.g., real-time & hybrid systems, RTL designs and microcode, software– by exploiting SMT technology.
    
  Currently my main interests are on the application of Optimization Modulo Theories (OMT) to the verification of systems.
• Modeling and Formal Reasoning with Software Requirements.
  Goal models have been widely used in Computer Science to represent software requirements, business objectives, and design quality. Since 2002 I am been working on formalizing Goal Models and on applying automated reasoning techniques (SAT, SMT and OMT) so that to provide tools for modeling and reasoning with goal models within the TROPOS methodology. Recently my research focuses on modeling and reasoning with constrained goal models, which extend goal models with SMT constraints, so that to (i) allow to associate resources and quantitative attributes to goals, tasks, requirements and assumptions so that to find optimal realizations, and to (ii) allow for representing and reasoning on the evolution of goal models, minimizing the effort of change. In both cases the OMT tool OptiMathSAT is used as automated-reasoning backend.

• Quantum Computing.
  I'm currently collaborating with D-Wave System Inc. on solving NP-Hard problems via Quantum Annealing via encoding into Ising Models. Some results have already been published.
• Probabilistic Reasoning via Weighted Model Integration.
  Recently I have given important contributions on SMT-based Weighted Model Integration, a very-effective framework for probabilistic reasoning.

• SAT for non-CNF formulas
• Decision procedures for modal and description logics.
• Planning.
• Abstraction in theorem proving