About

Sayan Mitra is a professor in the Electrical and Computer Engineering department at the University of Illinois Urbana-Champaign and an affiliate professor in the Computer Science department. He earned his Ph.D. from MIT in 2007 with a thesis titled "A Verification Framework for Hybrid Systems," under the supervision of Nancy Lynch. His academic background also includes a Master of Science from the Indian Institute of Science and a Bachelor of Engineering from Jadavpur University. His research interests encompass control theory, formal methods, AI and autonomy, cyber-physical computing, embedded systems, programming languages, and security and privacy. Mitra has authored or co-authored several books, including "Verifying Cyber-Physical Systems: A Path to Safe Autonomy." His scholarly work features numerous articles in prestigious journals and conference proceedings, focusing on topics such as hybrid automata, state estimation, multi-agent motion planning, controller synthesis, and formal verification of complex systems. Mitra's contributions significantly advance the understanding and development of verification frameworks and safety analysis for autonomous and cyber-physical systems.

Research topics

• Computer Science
• Artificial Intelligence
• Engineering
• Human–computer interaction
• Mathematics
• Computer Security
• Data science
• Simulation
• Transport engineering
• Theoretical computer science
• Real-time computing
• Programming language

Selected publications

• Minimal Information Control Invariance via Vector Quantization

  ArXiv.org · 2026-04-03

  articleOpen accessSenior author

  Safety-critical autonomous systems must satisfy hard state constraints under tight computational and sensing budgets, yet learning-based controllers are often far more complex than safe operation requires. To formalize this gap, we study how many distinct control signals are needed to render a compact set forward invariant under sampled-data control, connecting the question to the information-theoretic notion of invariance entropy. We propose a vector-quantized autoencoder that jointly learns a state-space partition and a finite control codebook, and develop an iterative forward certification algorithm that uses Lipschitz-based reachable-set enclosures and sum-of-squares programming. On a 12-dimensional nonlinear quadrotor model, the learned controller achieves a $157\times$ reduction in codebook size over a uniform grid baseline while preserving invariance, and we empirically characterize the minimum sensing resolution compatible with safe operation.

  PublisherOA PDF

• FalconApp: Rapid iPhone Deployment of End-to-End Perception via Automatically Labeled Synthetic Data

  arXiv (Cornell University) · 2026-04-21

  articleOpen accessSenior author

  Reliable perception for robotics depends on large-scale labeled data, yet real-world datasets rely on heavy manual annotation and are time-consuming to produce. We present FalconApp, an iPhone app with an end-to-end frontend-backend pipeline that turns a short handheld capture of a rigid object into a perception module for mask detection and 6-DoF pose estimation. Our core contribution is a rapid mobile deployment pipeline paired with a photorealistic auto-labeling workflow: from a user-captured video of an object, FalconApp reconstructs an editable GSplat asset, composites it with diverse photorealistic backgrounds, renders synthetic images with ground-truth masks and poses, trains the perception module, and deploys it back to the iPhone frontend. Experiments across five rigid objects with diverse geometry and appearance show that FalconApp produces usable perception models with about 20 minutes of synthetic-data generation and training per object on average, around 30 ms end-to-end on-device latency on iPhone, and better overall pose accuracy than a PnP baseline on 4 / 5 objects in both simulation and real-world evaluation.

  PublisherOA PDF

• Minimal Information Control Invariance via Vector Quantization

  arXiv (Cornell University) · 2026-04-03

  preprintOpen accessSenior author

  Safety-critical autonomous systems must satisfy hard state constraints under tight computational and sensing budgets, yet learning-based controllers are often far more complex than safe operation requires. To formalize this gap, we study how many distinct control signals are needed to render a compact set forward invariant under sampled-data control, connecting the question to the information-theoretic notion of invariance entropy. We propose a vector-quantized autoencoder that jointly learns a state-space partition and a finite control codebook, and develop an iterative forward certification algorithm that uses Lipschitz-based reachable-set enclosures and sum-of-squares programming. On a 12-dimensional nonlinear quadrotor model, the learned controller achieves a $157\times$ reduction in codebook size over a uniform grid baseline while preserving invariance, and we empirically characterize the minimum sensing resolution compatible with safe operation.

  PublisherDOI

• Active Localization of Unstable Systems with Coarse Information

  ArXiv.org · 2026-02-05

  articleOpen accessSenior author

  We study localization and control for unstable systems under coarse, single-bit sensing. Motivated by understanding the fundamental limitations imposed by such minimal feedback, we identify sufficient conditions under which the initial state can be recovered despite instability and extremely sparse measurements. Building on these conditions, we develop an active localization algorithm that integrates a set-based estimator with a control strategy derived from Voronoi partitions, which provably estimates the initial state while ensuring the agent remains in informative regions. Under the derived conditions, the proposed approach guarantees exponential contraction of the initial-state uncertainty, and the result is further supported by numerical experiments. These findings can offer theoretical insight into localization in robotics, where sensing is often limited to coarse abstractions such as keyframes, segmentations, or line-based features.

  PublisherOA PDF

• Active Localization of Unstable Systems with Coarse Information

  Open MIND · 2026-02-05

  preprintSenior author

  We study localization and control for unstable systems under coarse, single-bit sensing. Motivated by understanding the fundamental limitations imposed by such minimal feedback, we identify sufficient conditions under which the initial state can be recovered despite instability and extremely sparse measurements. Building on these conditions, we develop an active localization algorithm that integrates a set-based estimator with a control strategy derived from Voronoi partitions, which provably estimates the initial state while ensuring the agent remains in informative regions. Under the derived conditions, the proposed approach guarantees exponential contraction of the initial-state uncertainty, and the result is further supported by numerical experiments. These findings can offer theoretical insight into localization in robotics, where sensing is often limited to coarse abstractions such as keyframes, segmentations, or line-based features.

  DOI

• FalconApp: Rapid iPhone Deployment of End-to-End Perception via Automatically Labeled Synthetic Data

  arXiv (Cornell University) · 2026-04-21

  preprintOpen accessSenior author

  Reliable perception for robotics depends on large-scale labeled data, yet real-world datasets rely on heavy manual annotation and are time-consuming to produce. We present FalconApp, an iPhone app with an end-to-end frontend-backend pipeline that turns a short handheld capture of a rigid object into a perception module for mask detection and 6-DoF pose estimation. Our core contribution is a rapid mobile deployment pipeline paired with a photorealistic auto-labeling workflow: from a user-captured video of an object, FalconApp reconstructs an editable GSplat asset, composites it with diverse photorealistic backgrounds, renders synthetic images with ground-truth masks and poses, trains the perception module, and deploys it back to the iPhone frontend. Experiments across five rigid objects with diverse geometry and appearance show that FalconApp produces usable perception models with about 20 minutes of synthetic-data generation and training per object on average, around 30 ms end-to-end on-device latency on iPhone, and better overall pose accuracy than a PnP baseline on 4 / 5 objects in both simulation and real-world evaluation.

  PublisherDOI

• FalconGym: A Photorealistic Simulation Framework for Zero-Shot Sim-to-Real Vision-Based Quadrotor Navigation

  2025-10-19 · 1 citations

  articleSenior author

  We present a novel framework demonstrating zero-shot sim-to-real transfer of visual control policies learned in a Neural Radiance Field (NeRF) environment for quadrotors to fly through racing gates. Robust transfer from simulation to real flight poses a major challenge, as standard simulators often lack sufficient visual fidelity. To address this, we construct a photorealistic simulation environment of quadrotor racing tracks, called FalconGym, which provides effectively unlimited synthetic images for training. Within FalconGym, we develop a pipelined approach for crossing gates that combines (i) a Neural Pose Estimator (NPE) coupled with a Kalman filter to reliably infer quadrotor poses from single-frame RGB images and IMU data, and (ii) a self-attention-based multi-modal controller that adaptively integrates visual features and pose estimation. This multi-modal design compensates for perception noise and intermittent gate visibility. We train this controller purely in FalconGym with imitation learning and deploy the resulting policy to real hardware with no additional fine-tuning. Simulation experiments on three distinct tracks (circle, U-turn and figure-8) demonstrate that our controller outperforms a vision-only state-of-the-art baseline in both success rate and gate-crossing accuracy. In 30 live hardware flights spanning three tracks and 120 gates, our controller achieves a 95.8% success rate and an average error of just 10 cm when flying through 38 cm-radius gates.

  PublisherDOI

• 'Too Theoretical and Nowhere Near Interesting': Using a Tool to Increase Student Motivation for Formal Methods

  2025-06-13 · 1 citations

  articleOpen accessSenior author

  Using formal methods to evaluate software and hardware enhances system reliability, which is crucial for safety-critical applications such as airplanes and autonomous vehicles. Formal methods are mathematical modeling techniques that can be used to verify the safety of systems. The use of formal methods is limited in industry due to a shortage of trained engineers. Educators in formal methods often report that many students do not see the benefit of formal methods and perceive the involved math as not worth the effort for their future careers as software engineers. This study aims to understand the current state of student beliefs and how using a formal verification tool affects student motivation to learn about formal methods. We used an Expectancy Value Cost Lite survey to measure student motivation. Students completed this survey multiple times while designing algorithms to control vehicles in different scenarios, both with and without a formal verification tool. We found that students in an autonomy class are motivated to use formal methods. Although the findings are not statistically significant, we observed a slight increase in motivation after using the tool. Additionally, using a formal verification tool solely for modeling may contribute to increased motivation. These results suggest that incorporating tools into coursework may be a useful step in motivating more students to study formal methods and enter the workforce with these skills.

  PublisherDOI

• Indistinguishability in Localization and Control with Coarse Information

  2025-05-06

  articleOpen accessSenior author

  We study localization and control problems in which agent dynamics are described by difference or differential equations, while output measurements are collected at discrete times and given by finite-valued maps depending on possibly unknown landmark locations. Guided by the goal of understanding fundamental limitations imposed by such coarse measurements, we focus on characterizing indistinguishable states, i.e., agent-landmark pairs that produce identical observations under all control inputs. We show that indis-tinguishability relations can be checked automatically under mild assumptions and, being a special type of bisimulation, we develop an iterative algorithm for approximately computing them. We then introduce an analytical approach, rooted in observability theory of linear control systems, which iteratively computes a sequence of subspaces converging in finitely many steps to the indistinguishable subspace; a differential-geometric extension to nonlinear systems is also outlined.

  PublisherOA PDFDOI

• Reachability for Nonsmooth Systems with Lexicographic Jacobians

  Lecture notes in computer science · 2025-01-01

  book-chapterOpen accessSenior author

  Abstract Reachability analysis for dynamical systems typically relies on the system’s Jacobian to bound sensitivity of solutions. This method fails for nonsmooth dynamical systems as the Jacobian becomes undefined at the points where the vector field is non-differentiable. Such models can be hybridized by gluing together several smooth subsystems or modes via transitions, but the accuracy of reachability degrades when reachable sets are propagated across the mode boundaries. We propose an alternative approach based on lexicographic differentiation . Lexicographic differentiation was introduced by Nesterov as a foundation for calculus for nonsmooth functions. Our algorithm computes linear bounds on sets of lexicographic Jacobians, which give bounds on trajectory sensitivities. This avoids hybridization, eliminates mode transition computations, and yields more accurate reachsets. On nonsmooth models, our method improves accuracy on average by 50%, compared to hybrid algorithms. It is also one of the first methods to effectively handle reachability of ReLU neural ODEs.

  PublisherOA PDFDOI

Recent grants

• FMitF: Collaborative Research: Track I: Predictive Online Safety Analysis from Multi-hop State Estimates for High-autonomy on Highways

  NSF · $489k · 2019–2023

• II-New: CyPhyHouse: A Laboratory for Evolving Distributed and Mobile Cyber-Physical Systems Research

  NSF · $626k · 2016–2021

• CSR: Small: Verifying Simulink-Stateflow models

  NSF · $500k · 2010–2015

• CAREER: Algorithms and Verification for Reliable Distributed Cyber-Physical Systems

  NSF · $475k · 2011–2018

• CSR: Small: From Simulations to Proofs for Cyberphysical Systems

  NSF · $515k · 2014–2018

Frequent coauthors

• Chuchu Fan

  Massachusetts Institute of Technology

  36 shared

• Hussein Sibai

  25 shared

• Yangge Li

  22 shared

• Nancy Lynch

  21 shared

• Geir E. Dullerud

  University of Illinois Urbana-Champaign

  21 shared

• Mahesh Viswanathan

  University of Illinois Urbana-Champaign

  20 shared

• Zhenqi Huang

  Central South University

  19 shared

• Chiao Hsieh

  University of Illinois Urbana-Champaign

  18 shared

Education

• PhD, EECS

  Massachusetts Institute of Technology

  2007

• MS, CSA

  Indian Institute of Science

  2001

• Bachelor of Engineering, Electrical Engineering

  Jadavpur University

  1999

Awards & honors

• Celebration of Excellence 2026
• Celebration of Excellence 2025
• Celebration of Excellence 2024
• Celebration of Excellence 2023
• Celebration of Excellence 2022