Roberto Sebastiani - research interests
My research focuses on Formal Verification (in particular, model
Automated Reasoning (in particular SAT and SMT) and
and their applications. My current
My past research involved also:
- Satisfiability Modulo Theories (SMT) and its applications to
SMT is the problem of checking satisfiability of formulas in complex
theories which extend boolean satisfiability (typically decidable
subclasses of First-order logic). I'm one of the inventors of the
``lazy'' approach to
SMT (now state-of-the-art), which efficiently combines DPLL-based SAT
solvers with theory-specific
decision procedures. I have investigated
and developed many techniques for developing efficient decision
procedures for SMT in expressive theories (modal logics, description
logics, linear arithmetic on reals and integers) on top of boolean SAT
solvers. With my collaborators we have introduced the technique of
Delayed Theory Combination as an alternative to "Classic" Nelson-Oppen
combination technique for SMT solvers. Variants of this technique is now
implemented in all state-of-the-art SMT solvers.
We also have introduced the idea of Formal Verification of RTL circuit
designs and of timed and
hybrid systems based on SMT.
- Formal Verification, Model Checking.
My research in this field focuses on new techniques for model checking
with linear temporal logic (LTL)] and for bounded model checking. With
my coauthors, we have proposed for the first time an extension of
bounded model checking for the verification of real-time and hybrid
systems by means of SMT tools. From an application viewpoint, I have
worked on verification of real-word, industrial systems in
technology transfer projects by means of model checking
- Formal Reasoning in SW Specification.
I have worked on applying automated reasoning techniques (mostly SAT
and SMT) to goal models, a formalism used for requirements analysis
within the TROPOS SW engineering methodology.
- SAT for non-CNF formulas
- Decision procedures for modal and description logics.
in theorem proving
Roberto Sebastiani's home page.