I work in the area of formal methods, and my research interests include verification and synthesis of reactive systems, applications of formal methods to control and robotics, quantitative verification of probabilistic systems, and information-flow security.
My work addresses the analysis of complex system models (featuring infinite state spaces, partial observability, continuous dynamics, and probabilistic uncertainty) against correctness requirements formalized in expressive formal specification languages (describing the temporal behaviour and strategic abilities of systems). I am particularly interested in applications of formal methods to autonomous systems, where my work addresses the limitations faced by autonomous control due to imperfect sensing and stochastic disturbances.