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, and Abstraction in theorem proving.