My work focuses on formal methods, in particular
model checking using Satisfiability Modulo Theories (SMT) for different systems (hybrid systems and embedded software) and on program analysis.
An SMT-based symbolic model checker for hybrid systems
A symbolic model checker for finite- and infinite-state systems.
An open source symbolic model checker for finite-state systems.
A verification tool for event-driven application programming protocols.
A tool for mining programming patterns conserved across source code repositories.
A Semi-algebraic ABstrAcTor for Hybrid systems.