publications and preprints
2024
Optimal runtime assurance via reinforcement learning Kristina Miller, Chris Zeitler, William Shen, Kerianne Hobbs, Sayan Mitra, John Schierman, and Mahesh Viswanathan. To appear in IEEE/ACM ICCPS International Conference on Cyberphysical Systems (ICCPS 2024), 2024.Assuring safety of vision-based swarm formation control Chiao Hsieh*, Yubin Koh, Yangge Li, and Sayan Mitra. To appear in American Control Conference (ACC), 2024.
Guaranteed safe satellite guidance and navigation using reachability based switching controllers Kristina Miller, Sean Phillips, and Sayan Mitra. To appear in American Control Conference (ACC), 2024.
2023
RTAEval: A framework for evaluating runtime assurance logic. Kristina Miller, Christopher K. Zeitler, William Shen, Sayan Mitra, and Mahesh Viswanathan. In proceedings of the 21st Intl. Symposium on Automated Technologies for Verification and Analysis (ATVA), pp 302–313, 2023. 2023.[Online] [Local PDF] [Code]
Parallel and incremental verification of hybrid automata with Ray and Verse Haoqing Zhu, Yangge Li, Keyi Shen, and Sayan Mitra. In Proceedings of the 21st Intl. Symposium on Automated Technologies for Verification and Analysis (ATVA), pp 95–114, 2023.
[Online] [Local PDF] [Code]
Safety of the Stanley controller with curved lanes and noisy perception Hongyi Li and Sayan Mitra. In the Proceedings of the 62nd IEEE Conference on Decision and Control (CDC), 2023.
[Local PDF]
Perception Contracts for Safety of ML-Enabled Systems. Angello Astorga, Chiao Hsieh, P. Madhusudan, and Sayan Mitra. In the Proceedings of Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2023), pp 2196–2223. ACM
[Online] [Local PDF] [Bibtex]
HyHooVer: Verification and Parameter Synthesis in Stochastic Systems with Hybrid State Space Using Optimistic Optimization. Negin Musavi, Dawei Sun, Sayan Mitra, Geir E. Dullerud, and Sanjay Shakkottai. To appear in Open Journal of Control Systems (OJ-CSYS), 2023.
[Online]
Verse: A Python library for reasoning about multi-agent hybrid system scenarios. Yangge Li, Haoqing Zhu, Katherine Braught, Keyi Shen, Sayan Mitra. In the Proceedings of Computer Aided Verification (CAV), Paris, 2023.
[arxiv] [PDF] [Local PDF] [Code]
State Estimation of Continuous-time Dynamical Systems with Uncertain Inputs with Bounded Variation: Entropy, Bit Rates, and relation with Switched Systems. Hussein Sibai and Sayan Mitra. In IEEE Transactions on Automatic Control, Number 21-0591, 2023.
[Online] [Local PDF]
Symmetry-based Abstractions for Hybrid Automata. Hussein Sibai and Sayan Mitra. IEEE Transactions on Automatic Control, 2023.
[Online] [Local PDF]
Structural and Sequential Cause in Hidden Markov Models. Katherine Braught and Sayan Mitra. Working paper, CREST abstract, 2023. [Local PDF]
Abstractions for safety assurance of autonomous systems. Chiao Hsieh. PhD dissertation, Dept. of Computer Science, Illinois, May 2023.
[Local PDF]
Parallel and incremental algorithms in Verse hybrid system verification library.. Haoqing Zhu. Masters thesis, Dept. of Computer Science, Illinois, May 2023.
[Local PDF] [Code]
2022
Challenges in Rebooting Autonomy with Deep Learned Perception. Abraham, Mayne, Perez, Hsieh, Li, Oliveira, Yu, Sun, Mitra. Industry track paper in proceedings International Conference on Embedded Software (EMSOFT) 2022, Shanghai, 2022.[Online] [Code] [Local PDF] [Video]
Verifying Controllers with Vision-based Perception Using Safe Approximate Abstractions.Chiao Hsieh, Yangge Li, Dawei Sun, Keyur Joshi, Sasa Misailovic, and Sayan Mitra. In proceedings International Conference on Embedded Software (EMSOFT) 2022 and Special Issue of TCAD, volume 41(11), pages 4205-4216, November, 2022.
[Online] [Code] [Local PDF] [Video]
Multi-agent Motion Planning using Differential Games with Lexicographic Preferences. Kristina Miller and Sayan Mitra. To appear in the proceedings of the IEEE Conference on Decision and Control (CDC) 2022, Cancun, Mexico, 2022.
[Local PDF]
Programming Abstractions for Simulation and Testing on Smart Manufacturing Systems.Chiao Hsieh, Daniel Wu, Yubin Koh, and Sayan Mitra. In proceedings IEEE Intl. Conf. on Automation Science and Engineering (CASE), Mexico City, 2022.
[Bib] [Online] [Code] [Local PDF] [Video]
Technical Perspective: Model Structure Takes Guesswork Out of State Estimation.Sayan Mitra. CACM February 2022, Vol. 65 No. 2 Page 110, 2022.
[Online] [PDF] [Local PDF]
NeuReach: Learning Reachability Functions from Simulations.Dawei Sun and Sayan Mitra. In proceedings of Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS), LNCS volume 13243, 2022.
[Online] [Code] [Local PDF]
Multi-agent motion planning from signal temporal logic specifications.Dawei Sun, Jingkai Chen, Sayan Mitra, and Chuchu Fan. In Robotics and Autonomy Letters (RAL) and ICRA 2022, 2022.
[Online] [PDF] [Code] [Local PDF]
MLEFlow: Learning from history to improve load balancing in Tor.Hussein Darir, Hussein Sibai, Chin-Yu Cheng, Nikita Borisov, Geir E. Dullerud, Sayan Mitra. Proc. Priv. Enhancing Technologies (PoPET) 2022(1), pages 75-104, 2022.
[PDF] [Local PDF]
Controller synthesis for linear system with reach-avoid specifications. Chuchu Fan, Zengyi Qin, Umang Mathur, Qiang Ning, Sayan Mitra, and Mahesh Viswanathan. In IEEE Transactions in Automatic Control (TAC), volume 67(4), pages 1713-1727, 2022.
[PDF] [Local PDF] [Code]
Symmetry for boosting algorithmic proofs of cyber-physical systems. Hussein Sibai and Sayan Mitra. In IEEE Computer Magazine (Algorithms column),55(10):88-93 Oct, 2022
[PDF]
2021
Verifying cyber-physical system: A path to safe autonomy. Sayan Mitra. MIT Press, 2021.[MIT Press] [Amazon] [Slides]
SceneChecker: Boosting scenario verification using symmetry abstractions. Hussein Sibai, Yangge Li and Sayan Mitra. Computer Aided Verification, CAV 21, 2021.
[PDF] [Full version] [Code]
HooVer: A framework for verification and parameter synthesis in stochastic systems using optimistic optimization. Negin Musavi, Dawei Sun, Sayan Mitra, Geir Dullerud, and Sanjay Shakkottai. 2021 IEEE Conference on Control Technology and Applications, CCTA 21, San Diego, August 2021.
[PDF] [Local PDF] [Code]
SkyTrakx: A toolkit for simulation and verification of unmanned air-traffic management (UTM) systems. Chiao Hsieh, Hussein Sibai, Hebron Taylor, Yifeng Ni, & Sayan Mitra. IEEE International Intelligent Transportation Systems Conference (ITSC), 2021.
[local PDF] [Code] [Slides] [Video]
Continuous integration and testing for autonomous racing in simulation. Minghao Jiang. Masters thesis, Department of Electrical and Computer Engineering, UIUC,2021.
[local PDF] [PDF]
Planning in dynamic and partially unknown environments. Kristina Miller, Chuchu Fan, and Sayan Mitra. Accepted for publication in Proceedings of 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS'21), July 7-9, 2021.
[PDF] [Code]
Egocentric abstractions for verification of distributed cyber-physical systems. Sung Woo Jeon and Sayan Mitra. In IEEE Workshop on the Internet of Safe Things (SafeThings'21), co-located with Oakland, 2021. Best paper award.
[PDF] [Code]
HIOA-CPS: Combining hybrid input/output automaton and game theory for security modeling of cyber-physical systems. Mustafa Abdallah, Sayan Mitra, Shreyas Sundaram and Saurabh Bagchi. Accepted for IEEE Workshop on the Internet of Safe Things (SafeThings'21), co-located with Oakland, 2021.
[PDF] [Code]
Continuous integration and testing for autonomous racing software: An experience report from GRAIC. Minghao Jiang, Kristina Miller, Dawei Sun, Zexiang Liu, Yixuan Jia, Arnab Datta, Necmiye Ozay, and Sayan Mitra. Presented at ICRA 2021 Workshop on Opportunities and Challenges in Autonomous Racing.
[PDF] [Code]
Fast and guaranteed safe controller synthesis for aerial vehicle models. Chuchu Fan, Kristina Miller and Sayan Mitra. AIAA Scitech, 2021.
[PDF]
Accelerating verification of cyber-physical systems using symmetry. Hussein Sibai. PhD thesis, Department of Electrical and Computer Engineering, UIUC, 2021.
[PDF]
Software tools for scenario verification of autonomous systems exploiting dynamical symmetries. Yangge Li. Masters thesis, Illinois, 2021.
[PDF]
2020
Koord: a language for programming and verifying distributed robotics applications. Ritwika Ghosh, Chiao Hsieh, Sasa Misailovic, and Sayan Mitra. OOPSLA, 2020.[PDF] [Code] [Video]
Fast and guaranteed safe controller synthesis for nonlinear vehicle models. Chuchu Fan, Kristina Miller, and Sayan Mitra. CAV, 2020.
[PDF] [Local PDF] [Slides pptx] [Code] [Video]
Online monitoring for safe pedestrian-vehicle interactions., Peter Du, Zhe Huang, Tianqi Liu, Ke Xu, Qichao Gao, Hussein Sibai, Katherine Rose Driggs-Campbell, Sayan Mitra. IEEE ITSC, 2020.
[PDF] [Local PDF] [Video]
Multi-agent safety verification using symmetry Transformations, Hussein Sibai, Navid Mokhlesi, Chuchu Fan, and Sayan Mitra. 26th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Dublin.
[PDF] [Local PDF]
CyPhyHouse: A programming, simulation, and deployment toolchain for heterogeneous distributed coordination, Ritwika Ghosh, Joao P. Jansch-Porto, Chiao Hsieh, Amelia Gosse, Minghao Jiang, Hebron Taylor, Peter Du, Sayan Mitra, Geir Dullerud, ICRA, 2020, Paris, France.
[PDF] [Local PDF] [Code] [Video]
2019
Dione: A protocol verification system built with Dafny for I/O automata, Chiao Hsieh and Sayan Mitra, Integrated Formal Methods - 15th International Conference, {IFM} 2019, editors, Wolfgang Ahrendt and Silvia Lizeth and Tapia Tarifa, pages 227--245, Springer, 2019.[PDF] [Local PDF] [Slides] [Code]
Formal methods for safe autonomy: data-driven verification, synthesis, and applications, Chuchu Fan, PhD Thesis, Department of Electrical and Computer Engineering, UIUC, 2019. Winner of ACM Doctoral Dissertation Award 2020 (News release)
[PDF] [PDF local]
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] [Amazon]
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), Taipei, October 27-31, 2019. LNCS 11781. Nominated for Best Paper Award.
[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] [Docs] [Video]
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]
Data-driven formal reasoning and their applications in safety analysis of vehicle autonomy features, C. Fan, B. Qi, & S. Mitra, IEEE Design & Test, volume 35 (3), pages 31-38, June 2018.
[PDF] [Local PDF] [Code] [Docs]
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] [Video] [Docs]
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] [Code]
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] [Bibtex]
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] [Bibtex]
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] [Bibtex]
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] [Bibtex]
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] [Bibtex]
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] [Bibtex]
A verification framework for hybrid systems, S. Mitra, PhD Thesis, MIT, 2007.
[PDF] [Local PDF] [Bibtex]
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] [Bibtex]
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] [Bibtex]
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] [Bibtex]
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] [Bibtex]
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] [Bibtex]
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] [Bibtex]
Proving atomicity: an assertional approach, G. Chockler, N. Lynch, S. Mitra & J. Tauber, Proceedings of Nineteenth International Symposium on Distributed Computing (DISC05), LNCS, Volume 3724, 152 - 168, 2005.
[PDF] [Local PDF] [Bibtex]
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] [Bibtex]
Motion coordination using virtual nodes, N. Lynch, S. Mitra & T. Nolte, Proceedings of 44th IEEE Conference on Decision and Control (CDC05), 2005.
[Local PDF] [Bibtex]
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] [Bibtex]
2004
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, 2004.[PDF] [Local PDF] [Bibtex]
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. [PS] [Bibtex]
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] [Bibtex]
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] [PS] [Bibtex]
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] [Bibtex]
Developing strategies for specialized theorem proving about untimed, timed, and hybrid I/O automata, S. Mitra & M. Archer, STRATA Workshop,2003.
[Local PDF] [Bibtex]
2001
HIOA - A specification language for hybrid input/output automata, S. Mitra, Masters Thesis, IISC, 2001.[Local PDF]