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)



C2E2: A Verification Tool For Stateflow Models, P. S. Duggirala, S. Mitra & M. Viswanathan, , 2015.
 [Local PDF]

Bounded Verification with On-the-Fly Discrepancy Computation, C. Fan & S. Mitra, , 2015.


Differentially Private Distributed Optimization, Z. Huang, S. Mitra & N. Vaidya, International Converence on Distributed Computing and Networks (ICDCN), 2015.


Controller Synthesis for Linear Time-varying Systems with Adversaries, Z. Huang, Y. Wang, S. Mitra & G. Dullerud, , 2015.


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.
[PDF]  [Local PDF]

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.
 [Local PDF]

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]

Entropy-minimizing Mechanism for Differential Privacy of Discrete-time Linear Feedback Systems, Y. Wang, Z. Huang, S. Mitra & G. Dullerud, Conference on Decision and Control (CDC), 2014.
 [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]