My research focuses on the verification (mathematically proving correctness) and synthesis (correct-by-design construction) of complex reactive systems. These systems often operate under partial observability, involve probabilistic uncertainty, and must meet rich temporal and strategic specifications. Currently, I am developing logical and algorithmic foundations for the automatic synthesis of reactive software with provable correctness guarantees. This includes addressing key challenges such as handling rich data domains, satisfying expressive temporal specifications, and enforcing quantitative requirements.