1. Simulation-guided Formal Analysis
   Most real-world models of dynamical systems are too complex to formally analyze; however, scientists and engineers have always used numerical simulations to understand and analyze system behaviors. The question we wish to address is: how can we formally extend simulation-based analyses? In this broad area, we have been investigating Lyapunov and contraction analyses of dynamical systems and mining temporal requirements for complex models.
2. Falsification of Real-world Dynamical Systems
   Following the pioneering work of tools such as S-TaLiRo and Breach, an emerging trend is to use optimization-based approaches to find bugs in real-world dynamical systems. The key idea is this: formulate the bug-finding problem as minimizing the cost of an appropriate objective function over the space of inputs to the system under test. We continue investigation in this line of research, paying special attention to newer approaches to explore the input space, efficient cost computation, and optimizers tailored to a model's structure.
3. Requirement Engineering
   The perennial questions for any formal verification approach are: how to express formal requirements and how to simplify the task of writing requirements for a design engineer. We investigate the usefulness of real-time temporal logics to allow a requirement engineering framework to address both these concerns.