skip to main content

Sayan Mitra

Sayan Mitra
Sayan Mitra
Professor, Electrical and Computer Engineering
(217) 333-7824
266 Coordinated Science Lab

For more information

Education

  • Ph.D., MIT, 2007. Thesis title: "A Verification Framework for Hybrid Systems." Advisor: Nancy Lynch

Biography

Sayan is a Professor of ECE and an Affiliate Professor of CS at the University of Illinois, Urbana-Champaign. His book on verification of cyber-physical systems was published by MIT press in 2021. He received the National Science Foundation's CAREER Award, AFOSR Young Investigator Research Program Award, IEEE-HKN C. Holmes MacDonald Outstanding Teaching Award, a Siebel Fellowship, and several best paper awards.

Academic Positions

  • Postdoctoral Scholar, Center for Mathematics of Information, 2007-08
  • Summer Faculty Fellow, Air Force Research Laboratory, Kirtland, NM 2011

Teaching Statement

Research Statement

The goal our research is to develop algorithms and software tools for safe autonomous systems. We use techniques from theoretical computer science and control theory.

Graduate Research Opportunities

We are looking for graduate students with background in CS theory (formal methods, logic, automata theory, algorithms) and/or control theory. Solid programming skills & other mathematical background (e.g. stochastic processes) would be a plus. As an graduate researcher you will develop new verification and synthesis algorithms, build tools, and perform experiments in using these tools on real systems.

Undergraduate Research Opportunities

We are looking for juniors/seniors with solid programming skills (E.g., C/C++, Java, Matlab) and who intend to go to grad school in one of the related research areas. Preference will be given to those who can commit to working at least 6-8 hours a week for a couple of semesters. You will work closely with one of the graduate students towards developing software tools or applying them to verify a systems. This typically leads to an undergraduate thesis or publishable work. Take a look at some of the research projects.

Research Interests

Books Authored or Co-Authored (Original Editions)

Selected Articles in Journals

Articles in Conference Proceedings

  • Planning in dynamic and partially unknown environments. Kristina Miller, Chuchu Fan, and Sayan Mitra. In Proceedings of 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS'21), July 7-9, 2021.
  • Fast and guaranteed safe controller synthesis. Chuchu Fan, Kristina Miller, and Sayan Mitra. In Proceedings of 32nd Intl. Conf. on Computer Aided Verification (CAV 2020), Los Angeles, LNCS 12224, pages 629--652, Springer, 2020.
  • CyPhyHouse: A programming, simulation, and deployment toolchain for heterogeneous distributed coordination. Ritwika Ghosh, Joao P. Jansch-Porto, Chiao Hsieh, Amelia Gosse, Minghao Jiang, Hebron Taylor, Peter Du, Sayan Mitra, Geir Dullerud. In Proceedings of Intl. Conf. on Robotics and Automation (ICRA 2020), Paris, 2020.
  • Online monitoring for safe pedestrian-vehicle interactions. Peter Du, Zhe Huang, Tianqi Liu, Ke Xu, Qichao Gao, Hussein Sibai, Katherine Driggs-Campbell, and Sayan Mitra. In Proceedings of 23rd IEEE Intl. Conf. on Intelligent Transportation Systems, Virtual conference, 2020.
  • Fast and guaranteed safe controller synthesis for aerial vehicle models. Chuchu Fan, Kristina Miller, and Sayan Mitra. AIAA Scitech, 2021.
  • Multi-agent safety verification using symmetry transformations. Hussein Sibai, Navid Mokhlesi, Chuchu Fan, and Sayan Mitra. In Proceedings of 26th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Dublin, Ireland, Springer 2020.
  • Dione: A protocol verification system built with Dafny for I/O automata. Chiao Hsieh and Sayan Mitra. In Proceedings of Integrated Formal Methods (iFM 2019), Bergen, Norway. LNCS vol 11918, pages 227-245, Springer, 2019.
  • Using symmetry transformations in equivariant dynamical systems for their safety verification. Hussein Sibai, Navid Mokhlesi, and Sayan Mitra. In Proceedings of 17th Automated Technology for Verification and Analysis (ATVA 2019), Taipei, Taiwan. LNCS vol 11781, pages 98-114, Springer 2019. Nominated for best paper award.
  • TightRope: Towards Optimal Load-balancing of Paths in Anonymous Networks. Hussein Darir, Hussein Sibai, Nikita Borisov, Geir E. Dullerud, and Sayan Mitra. In Proceedings of the Workshop on Privacy in the Electronic Society (WPES) held with the ACM CCS conference, 2018: 76-85
  • Controller synthesis made real: Reach-avoid specifications and linear dynamics. Chuchu Fan, Umang Mathur, Sayan Mitra, and Mahesh Viswanathan. In Proceedings of Computer Aided Verification (CAV 2018), Oxford, Springer, 2018.
  • Verified hybrid LQ control for autonomous spacecraft rendezvous. Nicole Chan and Sayan Mitra, In IEEE International Conference on Decision and Control (CDC`17), Melbourne, Australia, 2017.
  • DryVR: Data-driven verification and compositional reasoning for automotive systems. Chuchu Fan, Bolun Qi, Sayan Mitra, and Mahesh Viswanathan. In Proceedings of Computer Aided Verification (CAV), Heidelberg, 2017.
  • Optimal data rate for state estimation of switched nonlinear systems. Hussein Sibaie and Sayan Mitra. In the Proceedings of the 20th ACM International Conference on Hybrid Systems: Computation and Control, April 2017.  Nominated for best paper award .
  •  Differential privacy in control and network systems. J. Cortés, G. E. Dullerud, S. Han, J. Le Ny, S. Mitra, and G. J. Pappas. In the Proceedings of 55th IEEE Conference on Decision and Control (CDC), pages 4252-4272, December 2016, Las Vegas, NV. 
  • Entropy notions for state estimation and model detection with finite-data-rate measurements. Daniel Liberzon and Sayan Mitra. In the Proceedings of 55th IEEE Conference on Decision and Control (CDC), pages 7335–7340, December 2016, Las Vegas, NV. 
  •  Locally optimal reach set over-approximation for nonlinear systems. Chuchu Fan, James Kapinski, Xiaoqing Jin, and Sayan Mitra. In the Proceedings of ACM SIGBED Conference on Embedded Software (EMSOFT) 2016, Pittsburgh, PA. Nominated for best paper award. 
  •  Automatic reachability analysis for nonlinear hybrid models with C2E2. Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, and Parasara Sridhar Duggirala. In the Proceedings of 28th International Conference on Computer Aided Verification (CAV), LNCS 9779, Pages 531–538, Toronto, Springer 2016. 
  • Entropy and minimal data rates for state estimation and model detection. Daniel Liberzon and Sayan Mitra. In Proceedings of 19th ACM International Conference on Hybrid System: Computation and Control (HSCC 2016), Vienna, Austria.
  • Controller synthesis for linear time-varying systems with adversaries. Zhenqi Huang, Yu Wang, Sayan Mitra, and Geir Dullerud. In the Proceedings of the 55th IEEE Conference on Decision and Control (CDC 2015), Osaka, Japan, 2015.
  • Meeting a powertrain verification challenge. Parasara Sridhar Duggirala, Chuchu Fan, Sayan Mitra, and Mahesh Viswanathan. In the proceedings of Computer Aided Verification - 27th International Conference (CAV 2015), LNCS 9206, pages 536—543. San Francisco, July 18-24, 2015.
  • StarL: Towards a unified framework for programming, simulating and verifying distributed robotic systems. Yixiao Lin and Sayan Mitra. In the Proceedings of the 16th ACM SIG- PLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems, (LCTES 2015), Pages 1–10. Portland, OR, USA, June.
  • Bounded verification with on-the-fly discrepancy computation. Chuchu Fan and Sayan Mitra. In the proceedings of 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), Shanghai, China.
  • Progress on Powertrain Verification Challenge with C2E2. Chuchu Fan, Parasara Sridhar Duggirala, Sayan Mitra, and Mahesh Viswanathan. In Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH 2015) held as part of CPSWeek 2015. Robert Bosch Sponsored Best Results Award. 
  •  A Strategy for automatic verification of stabilization of distributed algorithms. Ritwika Ghosh∗ and Sayan Mitra. In the Proceedings of 35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015), Grenoble, France, June 2-4. LNCS 9039, pages 35-49, Springer 2015. Nominated for best paper award. 
  • Differentially Private Distributed Optimization. Zhenqi Huang, Sayan Mitra, and Nitin Vaidya. In the proceedings of the International Conference on Distributed Computing and Networks, January 2015.(Acceptance: 21%)
  • C2E2: A Verification Tool For Annotated Stateflow Models. Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan, and Matthew Potok. In the proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2015. (Acceptance 17%)
  • Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells. Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, and Marta Kwiatkowska. In the proceedings of the Computer-Aided Verification (CAV 2014), July 2014 (Part of the Vienna Summer of Logic, VSL 2014). Springer.(Acceptance 25%)
  • Proofs from Simulations and Modular Annotations. Zhenqi Huang and Sayan Mitra. In 17th International Conference on Hybrid Systems: Computation and Control (HSCC). Berlin, 2014. ACM press.
  • Verification of Annotated Models from Executions. Parasara Sridhar Duggirala, Sayan Mitra, and Mahesh Viswanathan. In the Proceedings of the International Conference on Embedded Software (EMSOFT 2013), Montreal, Canada, April 2013.
  • Static and Dynamic Analysis of Timed Distributed Traces. Parasara Sridhar Duggirala, Taylor Johnson, Adam Zimmerman, and Sayan Mitra. In the Proceedings of The 33rd IEEE Real-Time Systems Symposium (RTSS), 2012, IEEE press. (Acceptance: 23%, premier conference)
  • A Small Model Theorem for Rectangular Hybrid Automata Networks. Taylor Johnson and Sayan Mitra. In the Proceedings of 32nd IFIP International Conference on Formal Techniques for Distributed Systems: Formal Techniques for Networked and Distributed Systems (FORTE), Stockholm, Sweden, June 2012. LNCS Vol 7273, pages 18-34, Springer. (Acceptance 38%, premier conference) (received the best paper award out of 155 submissions in DisCoTec'12).
  • Lyapunov Abstractions for Verifying Inevitability of Hybrid Systems. Parasara S. Duggirala and Sayan Mitra. In the Proceedings of 15th International Conference on Hybrid Systems: Computation and Control (HSCC 2012), pages 115-124, Beijing, PRC. April 2012. ACM press.
  • Differentially Private Iterative Synchronous Consensus. Zhenqi Huang, Sayan Mitra and Geir Dullerud. In Proceedings of the Workshop on Differentially Private Iterative Synchronous Consensus in conjunction with the ACM CCS conference, Raleigh, NC, 2012. (Acceptance 29%)

Invited Lectures

Magazine Articles

  • Verifying Cyber-Physical Interactions in Safety-Critical Systems. Sayan Mitra, Tichakorn Wongpiromsarn, and Richard Murray. In a Special Issue of IEEE Security & Privacy Magazine on Safety-Critical Systems, June 2013.

Conferences Organized or Chaired

  • Organizing committee member for The Cyber-Physical Systems Week 2011, Chicago, USA.
  • Program committee member for The 14th International Conference on Hybrid Systems: Computation and Control (HSCC 2011), Chicago, USA.
  • PC member, ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2012), Beijing.
  • Session organizer for "Cyber-physical system verification" at 50th Annual Allerton Conference, 2012.
  • PC member, ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2013), Philadelphis, PA.
  • PC member, IEEE/ACM International Conference on Cyberphysical Systems(ICCPS 2013), Philadelphia, PA.
  • PC member, Special Session on Design of Cyber-Physical Systems at Euromicro conference on Digital System Design (DSD), Santander, Spain on 4-6 Sept 2013.

Other Scholarly Activities

  • Hybrid Abstraction Refinement Engine (HARE): A software tool for verification of hybrid systems has been developed (in C++) and released. Several verification case studies (approx. 10) have been performed.
  • Passel: A software tool for verifying networks of hybrid automata http://publish.illinois.edu/passel-tool/

Professional Societies

  • HKN
  • ACM
  • IEEE Senior member

Honors

  • National Science Foundation's Faculty Early Career Development (CAREER) Award (2011)
  • Air-Force Office of Scientific Research (AFOSR) Young Investigator Research Award (2012)
  • College of Engineering Dean's award for excellence in research (2018)
  • Student Chuchu Fan's PhD thesis nominated for the ACM Doctoral Dissertation Award from Illinois. The thesis was awarded the CSL Dissertation Award. (2020)

Teaching Honors

  • IEEE-Eta Kappa Nu's C. Holmes MacDonald Outstanding Electrical and Computer Engineering Teacher Award. (2013)

Courses Taught

  • CS 584 - Embedded System Verification
  • ECE 220 - Computer Systems & Programming
  • ECE 498 - Autonomous Systems
  • ECE 498 - Principles of Safe Autonomy
  • ECE 584 - Embedded System Verification
  • ECE 598 - Special Topics in ECE