Experience
Education
Bio
Main directions of my research:

Synthesis of inductive invariants for verification of program safety and termination,

Functional (Skolem) synthesis via lazy quantifier elimination and programming by example,

Relational verification and its applications to security analysis and automated parallelization,

SMT-based reasoning over Algebraic Data Types: synthesis of invariants and simulation relation.