smart-exhibit oldfashioned-list scholar.google dblp

Above: Abstract keyword cloud created with wordle.

Research Agenda

Broadly, the research activities in our group fall under: (a) foundations of distributed cyber-physical systems, (b) modeling and verification of hybrid systems, and (c) applications. [Read more]


If some of the following PDF links do not open in your browser, try right-clicking and then save link as. Here is a collaboration graph.


Publications and Preprints (reverse chronological order)



Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol, P. S. Duggirala, L. Wang, S. Mitra, C. Munoz & M. Viswanathan, International Conference on Formal Methods (FM 2014), Singapore, 2014.
[PDF]  [Local PDF]  [Slides]

Synthesis and Verification of Motor-Transmission Shift Controller for Electric Vehicles, H. Chen & S. Mitra, the Proceedings of the International Conference on Cyberphysical Systems (ICCPS 2014), 2014.
 [Local PDF]  [Slides]

Closing the Loop brings Embedded System Analysis Closer to Software, P. S. Duggirala, S. Mitra & M. Viswanathan, , 2014.


Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells, Z. Huang, C. Fan, A. Mereacre, S. Mitra & M. Kwiatkowska, Computer Aided Verification (CAV 2014), 2014.


Proofs from Simulations and Modular Annotations, Z. Huang & S. Mitra, 17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014), 2014. Nominated for DENSO Best Student Paper Award.
[PDF]  [Local PDF]  [Slides]

On the Cost of Differential Privacy in Distributed Control Systems, Z. Huang, Y. Wang, S. Mitra & G. Dullerud, The 3rd ACM International Conference on High Confidence Networked Systems (HiCoNS 2014) at CPSWeek, 2014.
[PDF]  [Local PDF]  [Slides]

Anonymized Reachability of Hybrid Automata Networks, T. T. Johnson & S. Mitra, Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS 2014), LVCS, 2014.


Proving Abstractions of Dynamical Systems through Numerical Simulations, S. Mitra, Hot Topics in Science of Security (HOTSOS), 2014.
 [Local PDF]  [Slides]

Developing Programming Abstractions for Cyberphysical Systems, S. Mitra, , 2014. A position paper, for NSF Workshop on Transportation Cyberphysical Systems.
 [Local PDF]

StarL for programming reliable robotic networks, A. Zimmerman, , 2013. MS Thesis, UIUC..
[PDF]  [Local PDF]

Verificationcation of Annotated Models from Executions, P. S. Duggirala, S. Mitra & M. Viswanathan, Proceedings of International Conference on Embedded Software (EMSOFT 2013), 1-10, 2013.
[PDF]  [Local PDF]  [Slides]

Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Application to Aerospace Systems, T. Johnson & S. Mitra, Proceedings of Infotech@AIAA, 2013.
 [Local PDF]

Safe and Stabilizing Distributed Traffic Control, T. Johnson & S. Mitra, , 2013. Under review.
 [Local PDF]

Uniform Verification of Safety for Parameterized Networks of Hybrid Automata, T. T. Johnson, , 2013. PhD Thesis, UIUC.
 [Local PDF]

Verifying Cyber-Physical Interactions in Safety-Critical Systems, S. Mitra, T. Wongpiromsarn & R. M. Murray, IEEE Security & Privacy , Volume 11, 28-37, 2013.
[PDF]

Hybrid Automata-based CEGAR for Rectangular Hybrid Systems, P. Prabhakar, P. S. Duggirala, S. Mitra & M. Viswanathan, the Proceedings of 14th International Conference on Verification, Model Checking, and Abstract Interpretation, 2013.
[PDF]  [Local PDF]

On Simulation-Based Verification of Nonlinear Nondeterministic Hybrid Systems, Z. Huang, , 2013. MS Thesis, UIUC.
[PDF]  [Local PDF]

Static and Dynamic Analysis of Timed Distributed Traces, P. S. Duggirala, T. Johnson, A. Zimmerman & S. Mitra, Proceedings of IEEE Real-Time Systems Symposium (RTSS 2012), 2012.
[PDF]  [Local PDF]  [Slides]

Lyapunov Abstractions for Inevitability of Hybrid Systems, P. S. Duggirala & S. Mitra, The 15th International Conference on Hybrid Systems: Computation and Control (HSCC 2012), Beijing, China., 2012.
[PDF]  [Local PDF]  [Slides]

Computing Bounded Reach Sets from Sampled Simulation Traces, Z. Huang & S. Mitra, The 15th International Conference on Hybrid Systems: Computation and Control (HSCC 2012), Beijing, China., 2012. Tool paper.
[PDF]  [Local PDF]  [Slides]

Trace-based Bounded Verification of Embedded Systems, Z. Huang & S. Mitra, , 2012. Under review.


Differentially Private Iterative Synchronous Consensus, Z. Huang, S. Mitra & G. Dullerud, Proceedings of the Workshop on Differentially Private Iterative Synchronous Consensus in conjunction with the ACM CCS conference 2012, 2012.
[PDF]  [Local PDF]  [Slides]

Compositional bounded reachability using time partitioning and abstraction, J. Green, , 2012. MS Thesis, UIUC..
[PDF]  [Local PDF]

Verifying Satellite Rendezvous and Conjunction Avoidance: A Formal Approach to Autonomy in Space, T. Johnson, J. Green, S. Mitra, R. Dudley & R. S. Erwin, International Conference on Formal Methods (FM), 2012.
 [Local PDF]  [Slides]

Parameterized Verification of Distributed Cyber-Physical Systems:An Aircraft Landing Protocol Case Study, T. Johnson & S. Mitra, ACM/IEEE Third International Conference on Cyber-Physical Systems, April 2012, Beijing, China, 2012.
 [Local PDF]  [Slides]

A Small Model Theorem for Rectangular Hybrid Automata Networks, T. Johnson & S. Mitra, IFIP International Conference on Formal Techniques for Distributed Systems joint international conference: 32nd Formal Techniques for Networked and Distributed Systems (FORTE)., LNCS, Volume 7273, 18--34, 2012. Best paper award..
[PDF]  [Local PDF]  [Slides]

Verification of Periodically Controlled Hybrid Systems: Application to An Autonomous Vehicle, T. Wongpiromsarn, S. Mitra, A. Lamperski & R. Murray, Special Issue of the ACM Transactions on Embedded Computing Systems (TECS) , Volume 11, Number S2, 2012.
[PDF]  [Local PDF]

Opportunistic clock synchronization for ad hoc networks, M. B. Carrasco, , 2011. MS Thesis, UIUC..
[PDF]  [Local PDF]

Sandboxing Controllers for Cyber-Physical Systems, S. Bak, K. Manamcheri, S. Mitra & M. Caccamo, Proceedings of 2nd IEEE/ACM International Conference on Cyber-physical systems (ICCPS 2011), 2011.
[PDF]  [Local PDF]

Verification of Distributed Systems with Local-Global Predicates, K. M. Chandy, B. Go, S. Mitra, C. Pilotto & J. White, Journal of Formal Aspects of Computing (FAC) , Volume 23, Number 5, 649-679, 2011.
[PDF]  [Local PDF]

Abstraction-Refinement for Stability, P. S. Duggirala & S. Mitra, Proceedings of 2nd IEEE/ACM International Conference on Cyber-physical systems (ICCPS 2011), 2011.
[PDF]  [Local PDF]

Safe Flocking in Spite of Actuator Faults using Directional Failure Detectors, T. Johnson & S. Mitra, Journal of Nonlinear Systems and Applications , Volume 2, Number 1-2, 73-95, 2011.
[PDF]  [Local PDF]

Stability of Digitally Interconnected Linear Systems, T. Johnson, S. Mitra & C. Langbort, Proceedings of 50th IEEE Conference on Decision and Control (CDC), 2011.
[PDF]  [Local PDF]  [Slides]

Translation of Simulink-Stateflow models to hybrid automata, K. Manamcheri Sukumar, , 2011. MS Thesis, UIUC..
[PDF]  [Local PDF]

Computing bounded epsilon-Reach Set with finite precision computations for a class of linear hybrid automata, K.-D. Kim, S. Mitra & P. R. Kumar, Proceedings of Hybrid Systems: Computation and Control (HSCC 2011), 2011.
[PDF]  [Local PDF]

A step towards verification and synthesis from Simulink/Stateflow models, K. Manamcheri, S. Mitra, S. Bak & M. Caccamo, Hybrid Systems: Computation and Control (HSCC 2011), 2011. Tool paper.
[PDF]  [Local PDF]

Hybrid Cyberphysical System Verification With Simplex Using Discrete Abstractions, S. Bak, A. Greer & S. Mitra, 16th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2010)., 2010. Nominated for Best paper award.
[PDF]  [Local PDF]

On The Theory of Stochastic Processors, P. S. Duggirala, S. Mitra, R. Kumar & D. Glazeski, Seventh International Conference on the Quantitative Evaluation of Systems (QEST 2010), 2010.
[PDF]  [Local PDF]

Safe and Stabilizing Distributed Flocking in Spite of Actuator Faults, T. Johnson & S. Mitra, , Number UILU-ENG-10-2204 (CRHC-10-02), 2010. Technical report UILU-ENG-10-2204 (CRHC-10-02).
[PDF]  [Local PDF]

Safe Flocking in spite of Actuator Faults, T. Johnson & S. Mitra, In proceedings of 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems, LNCS, 2010.
[PDF]  [Local PDF]

Safe and Stabilizing Distributed Cellular Flows, T. Johnson, S. Mitra & K. Manamcheri, Proceedings of IEEE Internaitonal Conference on Distributed Computing Systems (ICDCS 2010), 2010.
[PDF]  [Local PDF]

Bounded epsilon-Reachability of Linear Hybrid Automata with a Deterministic and Transversal Discrete Transition Condition, K.-D. Kim, S. Mitra & P. R. Kumar, Proceedings of The 49th IEEE Conference on Decision and Control (CDC), 2010.
[PDF]

Fault-tolerant distributed cyber-physical systems: two case studies, T. Johnson, , 2010. MS Thesis, UIUC..
[PDF]

Stability of Distributed Algorithms in the face of Incessant Faults, R. E. L. DeVille & S. Mitra, Proceedings of 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2009), 2009.
[PDF]  [Local PDF]  [Slides]

Self-stabilizing robot formations over unreliable networks, S. Gilbert, N. Lynch, S. Mitra & T. Nolte, Special Issue on Self-adaptive and Self-organizing Wireless Networking Systems of ACM Transactions on Autonomous and Adaptive Systems (TAAS) , Volume 4, Number 3, 1-29, 2009.
[PDF]  [Local PDF]

Hybrid input output automata for composable conveyor systems, S. Mitra & S. Sastry, 5th Annual IEEE International Conference on Automation Science and Engineering (CASE'09), 29-29, 2009.


On Convergence of Concurrent Systems under Regular Interactions, P. Prabhakar, S. Mitra & M. Viswanathan, 20th International Conference on Concurrency Theory (CONCUR 2009), LNCS, Volume 5710, 527-541, 2009.
[PDF]  [Local PDF]

Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle, T. Wongpiromsarn, S. Mitra, R. Murray & A. Lamperski, 12th International Conference Hybrid Systems: Computation and Control (HSCC 2009), 396-410, 2009.
[PDF]  [Local PDF]

Specifying and Proving Properties of Timed I/O Automata Using Tempo, M. Archer, H. Lim, N. Lynch, S. Mitra & S. Umeno, Design Automation for Embedded Systems , Volume 8, Number 1-2, 2008.
[PDF]  [Local PDF]

Self-stabilizing Mobile Robot Formations with Virtual Nodes, S. Gilbert, N. Lynch, S. Mitra & T. Nolte, 10th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2008), 188-202, 2008.
[PDF]  [Local PDF]  [Slides]

Convergence Verification: From Shared Memory to Partially Synchronous Systems, K. M. Chandy, S. Mitra & C. Pilotto, Formal Modeling and Analysis of Timed Systems (FORMATS`08), LNCS, Volume 5215, 217-231, 2008.
[PDF]  [Local PDF]  [Slides]

A Formalized Theory for Verifying Stability and Convergence of Automata in PVS, S. Mitra & K. M. Chandy, Theorem Proving in Higher Order Logics (TPHOLS 2008), 230-245, 2008.
[PDF]  [Local PDF]

Verifying Average Dwell Time of Hybrid Systems, S. Mitra, D. Liberzon & N. Lynch, ACM Transactions on Embedded Computing Systems , Volume 8, 2008.
[PDF]  [Local PDF]

Learning Cycle-Linear Hybrid Automata for Excitable Cells., R. Grosu, S. Mitra, P. Ye, E. Entcheva, I. V. Ramakrishnan & S. A. Smolka, Hybrid Systems: Computation and Control (HSCC 2007), 245-258, 2007.
[PDF]  [Local PDF]  [Slides]

A Verification Framework for Hybrid Systems, S. Mitra, , 2007. PhD Thesis.
[PDF]  [Local PDF]

Proving approximate implementation relations for Probabilistic I/O Automata., S. Mitra & N. Lynch, Electronic Notes in Theoretical Computer Science , Volume 174, Number 8, 71-93, 2007.
[PDF]  [Local PDF]

Trace-based Semantics for Probabilistic Timed I/O Automata, S. Mitra & N. Lynch, Hybrid Systems: Computation and Control (HSCC 2007), 718-722, 2007.
[PDF]  [Local PDF]

Specifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit , M. Archer, H. Lim, N. Lynch, S. Mitra & S. Umeno, In Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06), 2006.
[PDF]  [Local PDF]

Approximate simulations for task-structured probabilistic I/O automata, S. Mitra & N. Lynch, LICS workshop on Probabilistic Automata and Logics (PAul06), 2006.
[PDF]  [Local PDF]  [Slides]

Verifying Average Dwell Time by Solving Optimization Problems, S. Mitra, D. Liberzon & N. Lynch, Proceedings of Hybrid Systems: Computation and Control (HSCC 2006), 476-490, 2006.
[PDF]  [Local PDF]  [Slides]

Proving atomicity: an assertional approach, G. Chockler, N. Lynch, S. Mitra & J. Tauber, Proceedings of Nineteenth International Symposium on Distributed Computing (DISC'05), LNCS, Volume 3724, 152 - 168, 2005.
[PDF]  [Local PDF]

Translating timed I/O automata specifications for theorem proving in PVS, H. Lim, D. Kaynar, N. Lynch & S. Mitra, Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS'05), LNCS, Number 3829, 2005.
[PDF]  [Local PDF]  [Slides]

Path vector face routing: Geographic routing with local face information, B. Leong, S. Mitra & B. Liskov, Proceedings of 13th IEEE International Conference on Network Protocols (ICNP'05), 2005.
[PDF]  [Local PDF]

Motion coordination using virtual nodes, N. Lynch, S. Mitra & T. Nolte, Proceedings of 44th IEEE Conference on Decision and Control (CDC05), 2005.
 [Local PDF]

PVS Strategies for Proving Abstraction Properties of Automata., S. Mitra & M. Archer, Electronic Notes in Theoretical Computer Science , Volume 125, Number 2, 45-65, 2005.
[PDF]  [Local PDF]

Stability of hybrid automata with average dwell time: an invariant approach, S. Mitra & D. Liberzon, Proceedings of the 43rd IEEE Conference on Decision and Control, 2005.
[PDF]  [Local PDF]

Specifying and Proving Timing Properties with TIOA Tools, D. Kaynar, N. Lynch & S. Mitra, In the work in progress session of the 25th IEEE International Real-Time Systems Symposium (RTSS-WIP), 2004.


Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata, S. Mitra & M. Archer, STRATEGIES 2004, IJCAR Workshop on strategies in automated deduction, 2004.


Energy efficient connected clusters for mobile ad hoc networks, S. Mitra & J. Rabek, Proceedings of 3rd Annual Mediterranean Ad Hoc Networking Workshop (MED-HOC-NET'04), 2004.
 [Local PDF]

Developing Strategies for Specialized Theorem Proving about Untimes, Timed, and Hybrid I/O Automata, S. Mitra & M. Archer, STRATA 2003, 2003.
 [Local PDF]

Safety Verification of Model Helicopter Controller using Hybrid Input/Output Automata, S. Mitra, Y. Wang, N. Lynch & E. Feron, 6th International Workshop on Hybrid Systems: Computation and Control (HSCC 2003), 343-358, 2003.
[PDF]  [Local PDF]

HIOA - A Specification Language for Hybrid Input/Output Automata, S. Mitra, , 2001. MS Thesis, IISC..
[PDF]  [Local PDF]