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)



Entropy and minimal bit rates for state estimation and model detection, D. Liberzon & S. Mitra, IEEE Transactions on Automatic Control (TAC),2018.
[PDF]  [Local PDF]

Design and Verification of a Safe Autonomous Satellite Rendezvous Maneuver, N. Chan, , 2018.


Building DryVR: A Verification and Controller Synthesis Engine for Cyber-Physical Systems and Safety-Critical Autonomous Vehicle Features, B. Qi, , 2018.


Algorithmic Attack Synthesis using Hybrid Dynamics of Power Grid Critical Infrastructures, Z. Huang, S. Etigowni, S. Zonouz & S. Mitra, proceedings of IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 2018.
 [Local PDF]

A technique for verifying nonlinear analog and mixed-signal circuits with inputs, C. Fan, Y. Meng, J. Maier, E. Bartocci, S. Mitra & U. Schmid, proceedings of ADHS, Oxford, UK., 2018.
 [Local PDF]

Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics, C. Fan, U. Mathur, S. Mitra & M. Viswanathan, proceedings of 30th International Conference on Computer Aided Verification (CAV), 2018.
 [Local PDF]

Approximate Partial Order Reduction, C. Fan, Z. Huang & S. Mitra, proceedings of 22nd International Symposium on Formal Methods (FM), 2018.
 [Local PDF]

SDCWorks: A Formal Framework for Software Defined Control of Smart Manufacturing Systems, M. Potok, C.-Y. Chen, S. Mitra & S. Mohan, International Conference on Cyberphysical Systems (ICCPS 2018), 2018.
[PDF]  [Local PDF]  [Slides]

State Estimation for Dynamical Systems with Unknown Inputs: Entropy and Bit Rates, H. Sibai & S. Mitra, Hybrid Systems: Computation and Control (HSCC 2018), Porto, Portugal., 2018.
[PDF]  [Local PDF]  [Slides]

State estimation of switched nonlinear systems and systems with bounded inputs: entropy and bit rates, H. Sibai, , 2017.
[PDF]

Differential Privacy in Distributed Control Systems: Entropy Minimizing Mechanisms and Performance Trade-offs, Z. Huang, Y. Wang, S. Mitra & G. Dullerud, IEEE Trans. on Control of Network Systems, Special Issue on Secure Control of Cyber Physical Systems , Volume 4, Number 1, 118-130, 2017.
[PDF]  [Local PDF]

Bounded invariant verification for time-delayed nonlinear networked dynamical systems, Z. Huang, C. Fan & S. Mitra, IFAC Jounral on Nonlinear analysis , Volume 23, 211-229, 2017.
[PDF]  [Local PDF]

Verified hybrid LQ control for autonomous spacecraft rendezvous, N. Chan & S. Mitra, IEEE International Conference on Decision and Control (CDC`17), 2017.
[PDF]  [Local PDF]  [Slides]

Optimal data rate for state estimation of switched nonlinear systems, H. Sibai & S. Mitra, Hybrid Systems: Computation and Control (HSCC 2017), Pittsburgh, PA., 71-80, 2017. Nominated for best paper award..
[PDF]  [Local PDF]  [Slides]

DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems, C. Fan, B. Qi, S. Mitra & M. Viswanathan, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, 441-461, 2017.
[PDF]  [Local PDF]  [Slides]

Verifying safety of an autonomous spacecraft rendezvous mission, N. Chan & S. Mitra, ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, collocated with Cyber-Physical Systems Week (CPSWeek) on April 17, 2017 in Pittsburgh, PA, USA, 20-32, 2017.
[PDF]

Programming platform for distributed robotics: Primitives and Portability, Y. Lin, , 2016.
[PDF]

Compositional analysis of networked cyber-physical systems: Safety and Privacy, Z. Huang, , 2016.
 [Local PDF]

Locally Optimal Reach Set Over-approximation for Nonlinear Systems, C. Fan, J. Kapinski, X. Jin & S. Mitra, Proceedings of the 13th ACM-SIGBED International Conference on Embedded Software (EMSOFT), EMSOFT '16, 6:1-6:10, 2016. Nominated for best paper award..
[PDF]

Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2, C. Fan, B. Qi, S. Mitra, M. Viswanathan & P. S. Duggirala, International Conference on Computer Aided Verification (CAV), LNCS, Volume 9779, 531-538, 2016.
[PDF]  [Local PDF]

Entropy and minimal data rates for state estimation and model detection, D. Liberzon & S. Mitra, Hybrid System: Computation and Control (HSCC 2016), 2016.
[PDF]  [Local PDF]

Controller Synthesis for Linear Time-varying Systems with Adversaries, Z. Huang, Y. Wang, S. Mitra & G. Dullerud, Hot topics in Science of Security (HOTSOS), 2016.
[PDF]

Entropy notions for state estimation and model detection with finite-data-rate measurements, D. Liberzon & S. Mitra, Decision and Control (CDC), 2016 IEEE 55th Conference on, 7335-7340, 2016.
[PDF]  [Local PDF]

Differential privacy in control and network systems, J. Cortés, G. Dullerud, S. Han, J. Le Ny, S. Mitra & G. J. Pappas, Decision and Control (CDC), 2016 IEEE 55th Conference on, 4252-4272, 2016.
[PDF]

Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP, P. S. Duggirala, C. Fan, M. Potok, B. Qi, S. Mitra, M. Viswanathan, S. Bak, S. Bogomolov, T. Johnson, L. V. Nguyen & others, Control Applications (CCA), 2016 IEEE Conference on, 1024-1029, 2016.


Simulation-based Verification of Cardiac Pacemakers with Guaranteed Coverage, Z. Huang, C. Fan, A. Mereacre, S. Mitra & M. Kwiatkowska, IEEE Design and Test Special Issue, 32(5) , Volume 32, 27-34, 2015.
[PDF]  [Local PDF]

Safe and Stabilizing Distributed Traffic Control, T. Johnson & S. Mitra, Theoretical Computer Science (TCS) , Volume 579, 9-32, 2015.
[PDF]  [Local PDF]

Hybrid Automata-based CEGAR for Rectangular Hybrid Systems, P. Prabhakar, P. S. Duggirala, S. Mitra & M. Viswanathan, In Formal Methods in System Design (FMSD) , Volume 46, Number 2, 105--134, 2015.
[PDF]

Analyzing Cost of Securing Control Systems, Z. Huang, Y. Wang, S. Mitra & G. Dullerud, The Next Wave, 21(1) , Volume 21, 12-17, 2015.
[PDF]  [Local PDF]

Progress on Powertrain Verification Challenge with C2E2, C. Fan, P. S. Duggirala, S. Mitra & M. Viswanathan, Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH 2015), 2015. Robert Bosch sponsored best verification result award..
 [Local PDF]

A Strategy for Automatic Verification of Stabilization of Distributed Algorithms, R. Ghosh & S. Mitra, Proceedings of Formal Techniques for Distributed Systems (FORTE) - Joint IFIP WG 6.1 International Conference, LNCS, Volume 9039, 35-49, 2015. Nominated for best paper award. .
[PDF]  [Local PDF]

C2E2: A Verification Tool For Stateflow Models, P. S. Duggirala, S. Mitra & M. Viswanathan, Proceedings of 21st International Conference Tools and Algorithms for the Construction and Analysis of Systems TACAS 2015, London, UK, April 11-18, 2015., Lecture Notes in Computer Science, Volume 9035, 68-82, 2015.
[PDF]  [Local PDF]

Differentially Private Distributed Optimization, Z. Huang, S. Mitra & N. Vaidya, International Converence on Distributed Computing and Networks (ICDCN 2015), Goa, India, January 4-7, 2015, 4:1-4:10, 2015.
[PDF]  [Local PDF]  [Slides]

Meeting a Powertrain Verification Challenge, P. S. Duggirala, C. Fan, S. Mitra & M. Viswanathan, In the Proceedings of International Conference on Computer Aided Verification (CAV 2015), LNCS, Volume 9206, 536-543, 2015.
 [Local PDF]

Model Checking Tap Withdrawal in C. Elegans, M. A. Islam, R. DeFrancisco, C. Fan, R. Grosu, S. Mitra & S. A. Smolka, Hybrid Systems Biology - Fourth International Workshop, HSB 2015, Madrid, Spain, September 4-5, 2015., Lecture Notes in Computer Science, Volume 9271, 195-210, 2015.
[PDF]  [Local PDF]

Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm, Z. Huang, Y. Wang, S. Mitra, G. Dullerud & S. Chaudhuri, 54th IEEE Conference on Decision and Control, CDC 2015, Osaka, Japan, December 15-18, 2015, 7434-7439, 2015.
[PDF]  [Slides]

Bounded Verification with On-the-Fly Discrepancy Computation, C. Fan & S. Mitra, 13th Intl. Symposium on Automated Technology for Verification and Analysis (ATVA 2015), Sanghai, China., LNCS, Volume 9364, 446-463, 2015.
[PDF]  [Local PDF]

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

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]

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. Johnson & S. Mitra, Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS 2014), LNCS, 2014.
[PDF]  [Local PDF]

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]

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

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

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]  [Slides]

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]

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

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

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

On Simulation-Based Verification of Nonlinear Nondeterministic Hybrid Systems, Z. Huang, , 2013. MS Thesis, UIUC.
[PDF]  [Local 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 (VMCAI 2013), 2013.
[PDF]  [Local PDF]

Verification 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]

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]

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


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

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]

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]

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]

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]

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]

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]

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]

Translation of Simulink-Stateflow models to hybrid automata, K. Manamcheri, , 2011. MS Thesis, UIUC..
[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]

Opportunistic clock synchronization for ad hoc networks, M. B. Carrasco, , 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]

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]

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]

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]

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]

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]

Fault-tolerant distributed cyber-physical systems: two case studies, T. Johnson, , 2010. MS Thesis, UIUC..
[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]

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]

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]

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]

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]

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]

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]

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.


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]

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]

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]

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]

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]

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.

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]

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]

A Verification Framework for Hybrid Systems, S. Mitra, , 2007. PhD Thesis.
[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]

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]

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]

[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.

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]

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]

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

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]

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]

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.

[PDF]  [Local PDF]  [Slides]

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]

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

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