My research is about making software reliable. This can be achieved through robust and comprehensive verification techniques based on formal methods such as model checking and static analysis, through intelligent and correct-by-construction design of programs, and by helping programmers debug and repair faulty programs more effectively. After joining Toyota, I have shifted my research focus to cyberphysical systems -- these are systems where physical systems are controlled with the help of software. Study of such systems requires an understanding of hybrid dynamical systems and aspects of control theory, in addition to knowledge of formal models of computation from the traditional software world. Many critical systems in today's world are cyberphysical systems. For example, an automotive engine controlled by an electronic control unit, an avionics system, medical devices, biological systems, power grids, and many others. My current research focuses on mathematically analyzing such systems to verify their safety and reliability. In the past, I have been interested in verification of sequential and concurrent software programs, verifying logical properties of (data) structures, static analysis of programs, and techniques for automatic program synthesis and repair. Specialties: Hybrid Systems, Temporal Logic, Automata theory, Dynamical Systems, Model Checking, Program Synthesis, Program Repair.