Formal Methods and Verification
Mathematically grounded specification, verification, falsification, and analysis techniques for cyber-physical and autonomous systems whose behavior must be checked against rigorous requirements.
Research
Research Directions
Learning-Enabled Cyber-Physical Systems
Methods for reasoning about systems that combine physical dynamics, software controllers, and learned components, with emphasis on safety, correctness, and interpretable evidence.
Temporal Logic and Runtime Monitoring
Specification languages and monitoring techniques for time-series behaviors, including signal temporal logic, temporal patterns, predictive monitoring, and online checks for system requirements.
Reinforcement Learning and Controller Synthesis
Specification-guided approaches for controller synthesis and reinforcement learning, including safe reinforcement learning, reward shaping, and formal reasoning about learned policies.
Multi-Agent Systems, Game Theory, and Autonomous Systems
Analysis and design questions arising in autonomous and multi-agent settings, including game-theoretic reasoning and verification-oriented approaches to coordinated system behavior.
LLMs and Perception-System Monitoring
Monitoring and evaluation directions for perception and AI-enabled systems, including requirements-focused checks for perception components and emerging large-language-model-enabled workflows.