- Ph.D., MIT, 2007. Thesis title: "A Verification Framework for Hybrid Systems." Advisor: Nancy Lynch
Sayan Mitra is an Associate Professor of Electrical and Computer Engineering. His research interests include formal methods, distributed computing, and mathematics for rigorous engineering of systems. He holds a PhD from MIT (2007), MSc from the IISc, Bangalore, and undergraduate degree from Jadavpur University, Kolkata. He was a postdoctoral fellow at CalTech, and has held visiting faculty positions at Oxford University, Air Force Research Laboratory (Kirkland), and TU Vienna. Sayan received the National Science Foundation's CAREER Award, AFOSR Young Investigator Research Program Award, IEEE-HKN C. Holmes MacDonald Outstanding Teaching Award, Samsung Global Research Outreach Award, and several best paper awards.
- Postdoctoral Scholar, Center for Mathematics of Information, 2007-08
- Summer Faculty Fellow, Air Force Research Laboratory, Kirtland, NM 2011
ECE 584 Verification of Embedded Computing Systems
ECE 598 Modeling and Verifying Embedded Computing Systems (Spring 2010);
ECE 190 Introduction to computing Systems (Fall 2009, Fall 2010, Fall 2011);
ECE 428/CS 425 Distributed Systems (Spring 2009, Spring 2012);
ECE 598 SM1 Modeling and Verification of Real-time and Hybrid Systems (Fall 2008).
The goal our research is to develop algorithms and software tools that enable the creation of reliable computing systems. Typical application domains include autonomous vehicles, traffic control systems, medical devices, control systems etc.
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.
- Automotive, aerospace, robotics & medical applications of the above
- Programming languages
- Formal verification and synthesis
- Distributed algorithms
- Embedded, real-time, and hybrid systems
- Formal methods and software verification
- Networking and distributed computing
- Programming languages
- Robotics and motion planning
- Software systems
Chapters in Books
- Specification language design for hybrid systems. Sayan Mitra and L. M. Patnaik. Computational Mathematics, Modeling and Algorithms, Edited by J. C. Misra. Alpha Science International, January 2003.
Selected Articles in Journals
- Simulation-based verification of cardiac pacemakers with guaranteed coverage. Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra and Marta Z. Kwiatkowska. IEEE Design & Test, volume 32(5), pages 27-34, 2015.
- Safe and Stabilizing Distributed Multi-Path Cellular Flows. Taylor T. Johnson and Sayan Mitra. Theoretical Computer Science, 2015, Elsevier.
- Hybrid Automata-based CEGAR for Rectangular Hybrid Systems. Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, and Mahesh Viswanathan. Formal Methods in Systems Design (FMSD), February 2015, Springer.
- Verification of Periodically Controlled Hybrid Systems: Application to An Autonomous Vehicle, Tichakorn Wongpiromsarn, Sayan Mitra,Andrew Lamperski, Richard Murray. In a Special Issue of the ACM Transactions on Embedded Computing Systems (TECS) 11(S2): 53 (2012).
- Specifying and proving properties of timed I/O automata using Tempo. Myla Archer, Hongping Lim, Nancy Lynch, Sayan Mitra, and Shinya Umeno Journal of Design Automation for Embedded Systems, Vol 2, Num 1-2, June 2008, Springer.
- Verifying Average Dwell Time of Hybrid Systems. Sayan Mitra, Daniel Liberzon and Nancy Lynch. In ACM Transactions in Embedded Computing Systems (TECS), Vol 8, Issue 1, pages 1-37 2008.
Articles in Conference Proceedings
- Entropy and minimal data rates for state estimation and model detection. Daniel Liberzon and Sayan Mitra. In 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 2016), 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.
- Diﬀerentially Private Iterative Synchronous Consensus. Zhenqi Huang, Sayan Mitra and Geir Dullerud. In Proceedings of the Workshop on Diﬀerentially Private Iterative Synchronous Consensus in conjunction with the ACM CCS conference, Raleigh, NC, 2012. (Acceptance 29%)
- Sandboxing Controllers for Cyber-Physical Systems. Stanley Bak, Karthik Manamcheri, Sayan Mitra, and Marco Caccamo. In the Proceedings of ACM/IEEE 2nd International Conference on Cyber-physical systems (ICCPS 2011), Chicago, IL, April 2011. (Acceptance 26%, premier conference)
- A step towards veriﬁcation and synthesis from Simulink/Stateﬂow models. Karthik Manamcheri, Sayan Mitra, Stanley Bak, and Marco Caccamo. In the Proceedings (as tool paper) of 14th International Conference on Hybrid Systems: Computation and Control (HSCC 2011), Chicago, IL, April 2011
- Safe and Stabilizing Distributed Cellular Flows. Taylor Johnson, Sayan Mitra, and M. Karthikeyan. In Proceedings of IEEE Internaitonal Conference on Distributed Computing Systems (ICDCS 2010). Pages 577 - 586, Genova, Italy. IEEE press. (Acceptance: 15%, premier conference)
- On Convergence of Concurrent Systems under Regular Interactions. Pavithra Prabhakar, Sayan Mitra, and Mahesh Viswanathan In the Proceedings of 20th In- ternational Conference on Concurrency Theory (CONCUR 2009). LNCS 5710, pages 527-541. Bologna, Italy, September, 2009. (Acceptance 28%, premier conference)
- Convergence Veriﬁcation: From Shared Memory to Partially Synchronous Systems. K. Mani Chandy, Sayan Mitra, and Concetta Pilotto. In Proceedings of 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’08), Saint Malo, France. LNCS 5215, pages 218-232, September 2008.
- Learning Cycle-linear hybrid automata of excitable cell models. Radu Grosu, Sayan Mitra, Pei Ye, Scott Smolka, Emilia Entcheva, and I.V. Ramakrishnan. In Proceedings of Hybrid Systems: Computation and Control (HSCC’07), April 2007.
- Abstractions for Safety and Stability Verification of Cyber-Physical Systems.
- Verification of Hybrid Systems through Abstractions and Approximations
- Abstraction-Refinement for Hybrid System Verification: An Air-traffic Control Case Study
- Replication-based fault tolerance in wireless distributed control.
- Programming mobile robots in the face of faults.
- 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
- C2E2 HyLink : A software tool that links Simulink/Stateflow models with hybrid system verification engines has been developed and released. http://publish.illinois.edu/c2e2-tool/
- 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/
- IEEE Senior member
- CMI Postdoctoral Fellow, California Institute of Technology (2007)
- National Science Foundation's Faculty Early Career Development (CAREER) Award (2011)
- Selected as Faculty Fellow for the 2011 Air Force Summer Faculty Fellowship Program (2011)
- Air-Force Office of Scientific Research (AFOSR) Young Investigator Research Award (2012)
- Best paper award at IFIP WG6.1 International Joint Conference FMOODS/FORTE (2012)
- Samsung Global Research Outreach (GRO) Award (2013)
- Nominated for Denso Best Paper Award given by Hybrid Systems: Computation and Control (2014) (2014)
- Honorable Mention for the IEEE-Eta Kappa Nu's C. Holmes MacDonald Outstanding Electrical and Computer Engineering Teacher Award. (2011)
- CS 584 - Embedded System Verification
- ECE 190 - Intro to Computing Systems
- ECE 198 - Computer Engineering II
- ECE 198 - Intro to Computer Eng II
- ECE 220 - Computer Systems & Programming
- ECE 584 - Embedded System Verification
- ECE 598 - Special Topics in ECE