Roberto Sebastiani - Research Interests
My research focuses on Formal Verification (in particular, model
Automated Reasoning (in particular SAT and SMT)
and their applications. My current main research
More recent research involves also:
- 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.
Currently my main interests are on the application of Optimization Modulo Theories (OMT) to the verification of systems.
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.
- 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.
My past research involved also:
- 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.
- <!A HREF =
in theorem proving
Roberto Sebastiani's home page.