Trustworthy AI-enabled Autonomous Systems Lab

Overview

Our lab conducts research in formal methods for the rigorous design and analysis of software systems in engineering applications, with a focus on AI-enabled cyber-physical and autonomous systems. Our work targets safety-critical domains such as automotive, aerospace, robotics, and agricultural automation. We investigate formal verification and synthesis techniques and tools that can provide guarantees of safety, security, correctness, reliability, and resilience in systems that integrate machine learning with physical processes. Our research lies at the intersection of computer science, mathematics, and engineering, spanning the development of theory, algorithms, and practical tools. Recent efforts focus on the verification of autonomous systems that incorporate neural networks for control, perception, and decision making, particularly systems that combine learning-enabled components with stochastic or hybrid dynamics. Key challenges we address include reachability analysis, neural network abstraction and reduction, conformance checking, and temporal and probabilistic verification. By bridging foundational formal methods with real-world autonomous and robotic applications, we aim to enable the safe and trustworthy deployment of intelligent systems in safety-critical domains.