Primary Research Area
- Software systems - Embedded, real-time, and hybrid systems
Ph.D., MIT, 2007. Thesis title: "A Verification Framework for Hybrid Systems." Advisor: Nancy Lynch
Sayan graduated from MIT in 2007 and spent one year as a post-doctoral researcher at the Center for Mathematics of Information of CalTech. Earlier, he completed MSc from the Indian Institute of Science, Bangalore and undergraduate degree in EE from Jadavpur University, Kolkata. He received the National Science Foundation's CAREER award in 2011, AFOSR Young Investigator Research Program Award in 2012. His research is aimed at developing algorithmic techniques for analyzing (and finding defects) in complex software systems that interact with physical processes.
- Postdoctoral Scholar, Center for Mathematics of Information, 2007-08
- Summer Faculty Fellow, Air Force Research Laboratory, Kirtland, NM 2011
For more information
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 4-5 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. Take a look at some of the research projects.
- Formal methods and applications in automotive, air-traffic control, medical systems.
- Formal verification of embedded, distributed, and real-time systems.
- Cyber-physical systems.
- Computer security, privacy, and information trust
- Decentralized and distributed control
- Discrete-event, switched and hybrid systems
- Distributed algorithms
- Distributed and peer-to-peer systems
- Embedded, real-time, and hybrid systems
- Embedded, real-time, and hybrid systems
- Fault tolerance and reliability
- Formal methods and software verification
- Multi-agent systems and robot control
- Networked control systems
- Programming languages
- Software systems
- System modeling and measurement
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
- 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).
- Verification of Distributed Systems with Local-Global Predicates. Mani Chandy, Brian Go, Sayan Mitra, Concetta Pilotto, and Jerome White. Journal of Formal Aspects of Computing, 23(5), pages 1-31. 2011. Springer.
- Safe Flocking in Spite of Actuator Faults using Directional Failure Detectors. Taylor Johnson and Sayan Mitra. To appear in the Journal of Nonlinear Systems and Applications (JNSA), 2011, Watam Press.
- Self-Stabilizing Robot Formations over Unreliable Networks. Seth Gilbert, Nancy Lynch, Sayan Mitra, and Tina Nolte. In a Special Issue of the ACM Transactions on Autonomous And Adaptive Systems (TAAS), volume 4, number 3, 2009.
- 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.
- Proving approximate implementation relations for Probabilistic I/O Automata Sayan Mitra and Nancy Lynch. In Electronic Notes in Theoretical Computer Science , Vol 174, Num 8, pages 71-93, 2007.
- PVS strategies for proving abstraction properties of automata. Sayan Mitra and Myla Archer. Electronic Notes in Theoretical Computer Science, Vol 125, Num 2, pages 45-65, 2005.
Articles in Conference Proceedings
- Hybrid Automaton-based CEGAR for Rectangular Hybrd Systems. Pavithra Prabhakar, Parasara S. Duggirala, Sayan Mitra, and Mahesh Viswanathan. In the Proceedings of International Conference on Veriﬁcation, Model Checking, and Abstract Interpretation (VMCAI), Rome, Italy 2013. (Acceptance: 30%)
- 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)
- Verifying Satellite Rendezvous and Conjunction Avoidance: A Formal Approach to Autonomy in Space. Taylor Johnson, Jeremy Green, Sayan Mitra, Rachel Dudley, and R. Scott Erwin. In the proceedings of Internation Conference on Formal Methods (FM) 2012, Paris, France. (Acceptance: 22%, 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).
- Parameterized Veriﬁcation of Distributed Cyber-Physical Systems: An Aircraft Landing Protocol Case Study. Taylor Johnson and Sayan Mitra. In the Proceedings of International Conference on Cyberphysical Systems (ICCPS 2012), pages 161 - 170, Beijing, PRC. April 2012. IEEE press. (Acceptance: 34%, premier conference)
- 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.
- Computing Bounded Reach Sets from Sampled Simulation Traces. Zhenqi Huang and Sayan Mitra. (Tool paper) In the Proceedings of 15th International Conference on Hybrid Systems: Computation and Control (HSCC 2012), Beijing, PRC. April 2012.
- 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%)
- Stability of Linear Systems with Quantized and Sampled Interconnections. Taylor Johnson, Sayan Mitra, and Cedric Langbort. In the Proceedings of 50th IEEE Conference on Decision and Control (CDC 2011), Orlando, FL, USA.
- Abstraction Reﬁnement for Stability. Parasara S. Duggirala and Sayan Mitra. In the Proceedings of ACM/IEEE 2nd International Conference on Cyber-physical systems (ICCPS 2011), Chicago, IL, April 2011. (Acceptance 26%, premier conference)
- 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
- Computing Bounded epsilon-Reach Set with Finite Precision Computations for a Class of Linear Hybrid Automata. Kyoung-Dae Kim, Sayan Mitra, and P. R. Kumar. In the Proceedings of 14th International Conference on Hybrid Systems: Computation and Control (HSCC 2011), Chicago, IL, April 2011.
- Safe Flocking in spite of Actuator Faults. Taylor Johnson and Sayan Mitra. In the Proceedings of 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems. LNCS 6366, pages 588-602. New York. September 2010.
- On the Theory of Stochastic Processors. Parasara Sridhar Duggirala, Sayan Mitra, Rakesh Kumar and Dean Glazeski. In Proceedings of 7th International Conference on Quantitative Evaluation of SysTems (QEST) 2010. LNCS, Williamsberg, VA, September 2010.
- 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)
- Bounded ε-Reachability of Linear Hybrid Automata with a Deterministic and Transversal Discrete Transition Condition. Kyoung-Dae Kim, Sayan Mitra, and P. R. Kumar. In Proceedings of the 49th IEEE Conference on Decision and Control (CDC 2010), Atlanta, GA.
- Hybrid Cyberphysical System Veriﬁcation With Simplex Using Discrete Abstractions. Stanley Bak, Ashley Greer, and Sayan Mitra. In the Proceedings of IEEE 16th Real-Time and Embedded Technology and Applications Symposium (RTAS 2010). (Nominated for best paper award. Acceptance: 22%, premier conference)
- Stability of Distributed Algorithms in the face of Incessant Faults. R. Lee DeVille and Sayan Mitra. In the Proceedings of 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS’09), LNCS 5873, pages 224- 237. Lyon, France. November 2009.
- 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)
- Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle. Tichakorn Wongpiromsarn, Sayan Mitra, Richard Murray and Andrew Lamperski. In the Pro- ceedings of 12th International Conference on Hybrid Systems: Computation and Control (HSCC 2009), San Francisco, CA. LNCS 5469, pages 396–410, March 2009.
- Self-stabilizing Mobile Robot Formations with Virtual Nodes. Seth Gilbert, Nancy Lynch, Sayan Mitra, Tina Nolte. In the Proceedings of 10th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS’08), Detroit, MI. LNCS 5340, pages 188–202. November 2008.
- 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.
- A Formalized theory for Stability and Convergence of Automata in PVS. Sayan Mitra and K. Mani Chandy. In Proceedings of 21st International Conference on Theorem Proving in High Order Logics (TPHOLs’08), Montreal, Canada. LNCS 5170, pages 230 – 245. August 2008.
- Trace-based semantics for probabilistic timed I/O automata. Sayan Mitra and Nancy Lynch. Extended abstract in Hybrid Systems: Computation and Control (HSCC’07), volume 4416 of LNCS, Springer 2007, April 2007.
- 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.
- Specifying and proving properties of Timed I/O Automata in the TIOA Toolkit. Myla Archer, Hongping Lim, Nancy Lynch, Sayan Mitra, and Shinya Umeno. In Proceedings of Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE’06). Napa, CA 2006. (One of the 4 papers selected for special issue of Journal on Design Automation of for Embedded Systems.)
- Approximate Simulations for Task-structured Probabilistic I/O Automata. Sayan Mitra and Nancy Lynch. In LICS workshop on Probabilistic Automata and Logics (PAuL’06), Seattle, WA, August 2006.
- Verifying Average Dwell time by solving optimization problems. Sayan Mitra, Daniel Liberzon, and Nancy Lynch. In Ashish Tiwari and Jo˜ao P. Hespanha, editors, Hybrid Systems: Computation and Control (HSCC’06), volume 3927 of LNCS, Santa Barbara, CA, March 2006.
- Translating Timed I/O Automata speciﬁcations for Theorem Proving in PVS. Hongping Lim, Dilsun Kaynar, Nancy Lynch, and Sayan Mitra. In Proceedings of Formal Modeling and Analysis of Timed Systems (FORMATS’05), volume 3829 of LNCS, Uppsala, Sweden, September 2005.
- Proving Atomicity: an Assertional Approach. Gregory Chockler, Nancy Lynch, Sayan Mitra, and Joshua Tauber. In Pierre Fraigniaud, editor, Proceedings of 19th International Symposium on Distributed Computing (DISC’05), volume 3724 of LNCS, pages 152 – 168, Cracow, Poland, September 2005. (Acceptance 20%, premier conference)
- Path Vector Face Routing: Geographic Routing with Local Face Information. Ben Leong, Sayan Mitra and Barbara Liskov. In Proceedings of 13th IEEE International Conference on Network Protocols (ICNP’05), Boston, Massachusetts, November 2005. (Acceptance 17%)
- Motion Coordination using Virtual Nodes. Nancy Lynch, Sayan Mitra, and Tina Nolte. In Proceedings of 44th IEEE Conference on Decision and Control (CDC’05), Seville, Spain, December 2005. Full version available as Technical Report MIT-LCS-TR-986.
- Stability of Hybrid Automata with Average Dwell Time: an Invariant Approach. Sayan Mitra and Daniel Liberzon. In Proceedings of the 43rd IEEE Conference on Decision and Control, Paradise Island, Bahamas, December 2004.
- Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata. Sayan Mitra and Myla Archer. In STRATEGIES 2004, IJCAR Affiliated Workshop on strategies in automated deduction, Cork, Ireland, July 2004.
- Safety Veriﬁcation of model Helicopter Controller using Hybrid Input/Output Automata. Sayan Mitra, Yong Wang, Nancy Lynch, and Eric Feron. In Hybrid System: Computation and Control (HSCC’03), volume 2623 of LNCS, Prague, Czech Republic, 2003. Full version available as Technical report MIT-LCS-TR-880.
- 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. To appear 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/
- 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)
Honorable Mention for the IEEE-Eta Kappa Nu's C. Holmes MacDonald Outstanding Electrical and Computer Engineering Teacher Award\/}. (2011)