Research interests

Formal verification of finite-state systems,

model-checking and bounded model-checking,

Decision procedures for first-order theories in the Satisfiability Modulo Theories (SMT) framework,

SAT and CSP,

Program equivalence checking,

Approximating computationally-hard problems in real-time.

Synthesis – from a temporal specification to a reactive system.