Faculty

Sayan Mitra

Sayan Mitra

Assistant Professor
266 Coordinated Science Lab, MC-228
1308 W. Main St.
Urbana, Illinois 61801
(217) 333-7824
Send Email

Phd, MIT, 2007

Research Statement:
The goal of my research is (a) to develop the foundations for analyzing distributed, real-time, and hybrid systems and (b) to facilitate design and verification of actual systems by creating software tools for synthesis, simulation, and verification. Typical applications include control systems, robotics, mobile networks, biological systems.

Teaching Statement:
ECE 428/CS 425 Distributed Systems (Spring 2009);
ECE 598 SM1 Modeling and Verification of Real-time and Hybrid Systems (Fall 2008).

Research Interests:

  • Embedded systems, distributed systems, real-time systems.
  • Formal methods, automated reasoning, logic.
  • Theory of hybrid and probabilistic system models and their applications in robotics, biology, etc.

For more information:
Distributed, Embedded and Hybrid Systems at ECE

Academic Positions

  • Postdoctoral Scholar, Center for Mathematics of Information, 2007-08

Honors, Recognition, and Outstanding Achievements

  • CMI Postdoctoral Fellow, California Institute of Technology (2007)

Journal Articles

  • Self-Stabilizing Robot Formations over Unreliable Networks. With Seth Gilbert, Nancy Lynch, and Tina Nolte. To appear in a Special Issue of the ACM Transactions on Autonomous And Adaptive Systems (TAAS) 2009.
  • PVS strategies for proving abstraction properties of automata. With Myla Archer. Electronic Notes in Theoretical Computer Science, Vol 125, Num 2, pages 45-65, 2005.
  • Proving approximate implementation relations for Probabilistic I/O Automata With Nancy Lynch. In Electronic Notes in Theoretical Computer Science , Vol 174, Num 8, pages 71-93, 2007.
  • Verifying Average Dwell Time of Hybrid Systems. With Daniel Liberzon and Nancy Lynch. In ACM Transactions in Embedded Computing Systems (TECS), Vol 8, Issue 1, pages 1-37 2008.
  • Specifying and proving properties of timed I/O automata using Tempo. With Myla Archer et al. Journal of Design Automation for Embedded Systems, Vol 2, Num 1-2, June 2008, Springer.

Articles in Conference Proceedings

  • Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle. With T. Wongpiromsarn, R. Murray and A. Lamperski. To appear in Proceedings of Hybrid Systems Computation and Control (HSCC`09).
  • A Formalized Theory for Verifying Stability and Convergence of Automata in PVS. With K. Mani Chandy. In Proceedings of Theorem Proving in High Order Logics (TPHOLs`08), LNCS 5170, 230--245, August 2008.
  • Convergence Verification: From Shared Memory to Partially Synchronous Systems. With K. Mani Chandy and Concetta Pilotto. In Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS'08) , LNCS 5215, pages 218-232, 2008.
  • Trace-based semantics of probabilistic timed I/O automata. With Nancy Lynch. In Hybrid Systems: Computation and Control (HSCC 07), LNCS 4416, pages 718-722, April 2007.
  • Learning cycle-linear hybrid automata of excitable cell models. With Radu Grosu, Pei Ye, Scott Smolka, Emilia Entcheva, and I.V. Ramakrishnan. In Hybrid Systems: Computation and Control (HSCC 07), LNCS 4416, pages 245-258, April 2007.
  • Approximate simulations for task-structured probabilistic I/O automata. With Nancy Lynch. LICS workshop on Probabilistic Automata and Logics (PAul06), Seattle, WA, August 2006.
  • Proving atomicity: an assertional approach. With Gregory Chockler, Nancy Lynch and Joshua Tauber. In Proceedings of 19th International Symposium on Distributed Computing (DISC'05), LNCS 3724, pages 152 - 168, September 2005.
  • Path vector face routing: Geographic routing with local face information. With Ben Leong and Barbara Liskov. In Proceedings of 13th IEEE International Conference on Network Protocols (ICNP'05), Boston, November 2005.
  • Translating timed I/O automata specifications for theorem proving in PVS. Hongping Lim, Dilsun Kaynar and Nancy Lynch. In Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS'05), LNCS 3829, Uppsala, Sweden, September 2005.
  • Safety verification of model helicopter controller using hybrid Input/Output automata. With Yong Wang, Nancy Lynch, and Eric Feron. In Hybrid System: Computation and Control (HSCC'03), LNCS volume 2623, pages 343-358. Springer. April 2003.

Invited Lectures

  • Programming mobile robots in the face of faults.

Conferences Organized or Chaired

  • Track chair for Formal Methods in Distributed Systems in the The 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2009).