Roberto Sebastiani - research interests
My research focuses on Formal Verification (in particular, model
checking) and
Automated Reasoning (in particular SAT and SMT) and
and their applications. My current
interests are:
- Satisfiability Modulo Theories (SMT) and its applications to
Formal verification.
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
techniques.
- 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.
My past research involved also:
- SAT for non-CNF formulas
- Decision procedures for modal and description logics.
- Planning.
- Abstraction
in theorem proving
Back to
Roberto Sebastiani's home page.