Other sources




Publications and Preprints


2019



Data-driven safety verification of complex cyber-physical systems, Chuchu Fan and Sayan Mitra, Design Automation for Cyber-Physical Systems, editors, Mohammad Abdullah Al Faruquqe and Arquimedes Canedo, pages 107-143, Springer, 2019.


[PDF]


Using symmetry transformations in equivariant dynamical systems for their safety verification, Hussein Sibai, Navid Mokhlesi and Sayan Mitra Proceedings of Automated Technology for Verification and Analysis (ATVA 2019), October 27-31, 2019.
[PDF] [Local PDF]


2018



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

Design and verification of a safe autonomous satellite rendezvous maneuver, N. Chan, UIUC Masters Thesis, 2018.
[PDF]

Building DryVR: A verification and controller synthesis engine for cyber-physical systems and safety-critical autonomous vehicle features, B. Qi, UIUC Masters Thesis, 2018.
[PDF] [Code]

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

Approximate partial order reduction, C. Fan, Z. Huang & S. Mitra, Proceedings of 22nd International Symposium on Formal Methods (FM), 2018.
[PDF] [Local PDF] [Slides]

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

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]


2017



State estimation of switched nonlinear systems and systems with bounded inputs: entropy and bit rates, H. Sibai, Masters Thesis, UIUC, 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]


2016



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

Compositional analysis of networked cyber-physical systems: Safety and Privacy, Z. Huang, Masters Thesis, UIUC, 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] [Tool]

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.


2015



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

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]


2014



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


2013



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, PhD Thesis, UIUC, 2013.
[PDF] [Local PDF]

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

On simulation-based verification of nonlinear nondeterministic hybrid systems, Z. Huang, Masters Thesis, UIUC, 2013.
[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] [Tool]

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]


2012



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]

Compositional bounded reachability using time partitioning and abstraction, J. Green, Masters Thesis, UIUC,2012.
[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.
[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.
[PDF] [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] [Tool]

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]


2011



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, Masters Thesis, UIUC, 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]

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


2010



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, Masters Thesis, UIUC, 2010.
[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]


2009



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]


2008



Verifying Average Dwell Time of Hybrid Systems, S. Mitra, D. Liberzon & N. Lynch, ACM Transactions on Embedded Computing Systems (ACM TECS), 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.
[PDF]

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]


2007



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, PhD Thesis, MIT, 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]

Learning cycle-linear hybrid automata for excitable cells, Radu Grosu, Sayan Mitra, Pei Ye, Emilia Entcheva, I. V. Ramakrishnan, Scott A. Smolka, Hybrid Systems: Computation and Control (HSCC 2007), 245-258, 2007.
[PDF] [Local PDF] [Slides]


2006



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]

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]


2005



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]


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

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]


2003



Safety verification of model helicopter controller using hybrid input/output automata, S. Mitra, Y. Wang, N. Lynch & E. Feron,Proceedings of 6th International Workshop on Hybrid Systems: Computation and Control (HSCC 2003), 343-358, Prague 2003.
[PDF] [Local PDF]

Developing strategies for specialized theorem proving about untimed, timed, and hybrid i/o automata, S. Mitra & M. Archer, STRATA Workshop,2003.
[Local PDF]


2001



HIOA - A specification language for hybrid input/output automata, S. Mitra, Masters Thesis, IISC, 2001.
[Local PDF]