About me [CV]

I am an Assistant Professor at University of North Carolina at Chapel Hill in the Department of Computer Science. I have recently moved from University of Connecticut in the Department of Computer Science and Engineering.  My research is at the intersection of Cyber-Physical Systems, Formal Methods, Autonomy, Embedded and Real-Time Systems, and Control Theory.

I am looking for bright and motivated graduate and undergraduate students. Send me an e-mail with your CV if you are interested.

I am currently working on developing frameworks for integrating safe autonomy into Cyber-Physical Systems. In my lab, we build, maintain, and prove the safety of autonomous CPS.

In the recent past, I have contributed to developing scalable techniques for safety verification of linear hybrid systems. This technique (available here) requires a mere n+1 simulations for computing the reachable set of n dimensional linear system. We have also implemented new constraint propagation techniques and dynamic aggregation techniques for verification of linear hybrid systems (available here and here). This work has won the Best Paper Award at ARCH Workshop, 2017.

My PhD thesis was about "Dynamic Analysis of Cyber-Physical Systems". I have developed C2E2, a tool that combines the scalability of simulations with the correctness guarantees of formal verification and applied it to analyze ALAS, an alerting system for a parallel aircraft landing protocol developed by NASA (details) and powertrain control systems in automobiles (details).

In the past, I have worked on Probabilistic Systems, Automatic Test Input Generation, and Decision Procedures.

News:

• [[February 2021]] Joint work with Clara Hobbs, Debayan Roy, F. Donelson Smith, Soheil Samii, James H. Anderson, and Samarjit Chakraborty titled "Perception Computing-Aware Controller Synthesis for Autonomous Systems" was presented by Clara Hobbs at DATE 2021.
  
  
• [[February 2021]] Joint work with Stanley Bak, Sergiy Bogomolov, Adam R Gerlach, and Kostiantyn Potomkin titled "Reachability of Black-Box Nonlinear Systems after Koopman Operator Linearization" has been accepted for publication at ADHS 2021. We proposed a technique to verify nonlinear systems by performing a Koopman linearization and converting them into high dimensional linear systems.
  
  
• [[February 2021]] I will be part of the Editorial Board of Real-Time Systems and Cyber-Physical Systems area for Journal of Systems Research (JSys).
  
  
• [[January 2021]] I will be part of the program committee of Languages, Compilers, Tools and Theory of Embedded Systems (LCTES) 2021.
  
  
• [[December 2020]] I will be part of the program committee of International Conference on Embedded Software (EMSOFT) 2021.
  
  
• [[October 2020]] Manish Goyal presents our work titled "NeuralExplorer: State Space Exploration of Closed Loop Control Systems Using Neural Networks" at ATVA 2020.
  
  
• [[July 2020]] Joint work with my student Edward Kim titled "Kaa: A Python Implementation of Reachable Set Computation Using Bernstein Polynomials" is presented at Applied Verification of Continuous and Hybrid Systems Workshop (ARCH) 2020. We provide a very easy to understand implementation of the Bernstein Polynomial based reachable set computation method for discrete nonlinear systems.
  
  
• [[July 2020]] More than 100 people have registered for International Workshop on Numerical Software Verification 2020 (website). We have successfully concluded the workshop with three keynote speakers on numerical software verification, neural networks, and reinforcement learning. Thanks for all those who submitted their papers to NSV 2020 and made the event successful.
  
  
• [[July 2020]] Manish presents our work "Generating Longest Counterexample: On the Cross-roads of Mixed Integer Linear Programming and SMT" at ACC 2020 virtually.
  
  
• [[June 2020]] Joint work with my student Manish Goyal titled "NeuralExplorer: State Space Exploration of Closed Loop Control Systems Using Neural Networks" has been accepted at ATVA 2020.
  
  
• [[April 2020]] CPS-IoT Week goes virtual. My student Abel presented our work on "Formalizing Traffic Rules for Uncontrolled Intersections" has presented our paper here at ICCPS 2020.
  
  
• [[March 2020]] COVID has been declared a national emergency.
  
  
• [[March 2020]] Joint work with my student Manish Goyal titled "NeuralExplorer: State Space Exploration of Closed Loop Control Systems Using Neural Networks" has been accepted as a poster at L4DC 2020.
  
  
• [[February 2020]] Charlotte Dorn has been selected as a SIGBED Scholar! Congratulations, Charlotte. She will be sponsored by SIGBED to attend CPS-IoT Week 2020. Read more about SIGBED Scholars program here.
  
  
• [[February 2020]] Joint work with my student Manish Goyal titled "Extracting Counterexamples Induced by Safety Violation in Linear Hybrid Systems" has been accepted to Automatica. This extends the notions of deepest and longest counterexamples to linear hybrid systems and develops algorithms for extracting them.
  
  
• [[March 2020]] Joint work with my student Manish Goyal and collaborator David Bergman titled "Generating Longest Counterexample: On the Cross-roads of Mixed Integer Linear Programming and SMT" has been accepted to ACC 2020.
  
  
  
• [[December 2019]] I will be a part of program committee for International Conference on Embedded Software (EMSOFT) 2020.
  
  
• [[December 2019]] Joint work with my student Abel Karimi titled "Formalizing Traffic Rules for Uncontrolled Intersections" has been accepted at ICCPS 2020. In this paper, we formalize the traffic rules to be followed by a vehicle at an intersection as sentences in first order logic and develop a traffic rules monitor for uncontrolled intersections.
  
  
• [[October 2019]] I will be a Co-Chair of International Workshop on Numerical Software Verification 2020 (website). Glad to share this responsibility with Peter Schrammel.
  
  
• [[October 2019]] I presented the paper on "Aggregation Strategies in Reachable Set Computation of Hybrid Systems" and my student Bineet Ghosh presented the paper on "Robust Reachable Set: Accounting for Uncertainties in Linear Dynamical Systems" at EMSOFT 2019.
  
  
• [[July 2019]] Two papers accepted to EMSOFT 2019. The first paper is a joint work with Stanley Bak titled "Aggregation Strategies in Reachable Set Computation of Hybrid Systems". We developed new techniques for aggregating sparse time reachable sets in HyLAA and analyzed two challenging case studies. The second paper is with my student Bineet Ghosh titled "Robust Reachable Set: Accounting for Uncertainties in Linear Dynamical Systems". We discovered a special class of uncertainties for which the safety analysis can be performed using bilinear inequalities.
  
  
• [[July 2019]] I will be presenting the paper "Incremental Minimization of Symbolic Automata" at VSTTE 2019.
  
  
• [[June 2019]] Join work with Jonathan Homburg (undergraduate student at UConn) titled "Incremental Minimization of Symbolic Automata" has been accepted to VSTTE 2019. We extended incremental minimization techniques for DFAs to work on Symbolic Automata.
  
  
• [[April 2019]] UNC won the F1Tenth Competition at CPS Week 2019!!! Congratulations to Nathan, Tanya, Abel, Manish, and Charlotte who were part of the team. Special thanks to Nathan who wrote this blog post on the algorithm we used. Charlotte maintains a Medium blog and penned a blog post on F1Tenth car.
  
  
• [[January 2019]] I have moved to University of North Carolina at Chapel Hill and joined the Computer Science Department.
  
  
• [[October 2018]] Renukanandan Tumu represents RacingHuskies at the F1Tenth Competition at ES Week 2018.
  
  
• [[August 2018]] Donals Sheehy presents out work on embedding trajectories into a Euclidean space at CCCG 2018.
  
  

• [[July 2018]] Manish presents his first paper at ADHS 2018.
  
  
• [[June 2018]] Joint work with Donald Sheehy titled "When Can We Treat Trajectories as Points?" has been accepted to CCCG 2018. We demonstrated a method to embed trajectories of dynamical system into euclidean space.
  
  
• [[April 2018]] RacingHuskies participated in F1Tenth Competition at CPS Week 2018 and we placed 2nd in the competition. Congratulations to Abol, Reynaldo, and Manish and especially to Nandan who traveled to Porto and did a great job!
  
  
• [[March 2018]] Work with my student Manish Goyal titled "On Generating a Variety of Unsafe Counterexamples for Linear Dynamical Systems" has been accepted to ADHS 2018. We managed to define new notations of deepest and longest counterexamples and developed techniques to extract them.
  
  
• [[April 2017]] Joint work with Stanley Bak titled "Simulation-Equivalent Reachability of Large Linear Hybrid Systems with Inputs" has been accepted to CAV 2017. We improved the scalability of verification by two orders of magnitude and verified a 10,000 dimensional system. For details, check out the paper here.
  
  
• [[April 2017]] Presented a paper titled "Rigorous Simulation-Based Analysis for Linear Hybrid Systems" at TACAS 2017. The techniques presented in the paper have been implemented in our tool called HyLAA.
  
  
• [[April 2017]] Stanley Bak presented our tool paper: "HyLAA: A Tool For Simulation-Equivalent Reachability for Linear Systems" at HSCC 2017. The paper has earned the repeatability evaluation badge. Feel free to download the tool HyLAA.
  
  
• [[April 2017]] Joint work with Stanley Bak won the Best Paper Award sponsored by Robert Bosch at ARCH Workshop, 2017.
  
  
• [[July 2016]] Chuchu Fan presented our paper "Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2" at CAV 2016. Feel free to try our tool C2E2 for verifying nonlinear hybrid systems such as lane changing systems and C-Elegans biological systems.
  
  
• [[July 2016]] Presented a paper titled "Parsimonious, Simulation Based Verification Of Linear Systems" at CAV 2016. Check out the new algorithm which verifies an n-dimensional linear system using a mere n+1 simulations here.
  
  
• [[December 2015]] Presented a paper titled "Analyzing Real-Time Linear Control Systems Using Software Verification" at RTSS 2015. Find out about our new technique to verify linear control systems in presence of real time scheduler here.
  
  
• [[August 2015]] I joined University of Connecticut CSE Department (UConnCSE).
  
  
• [[April 2015]] Join work with Chuchu Fan, Sayan Mitra, and Mahesh Viswanathan won the Most Promising Benchmark Result sponsored by Robert Bosch at ARCH Workshop, conducted as part of CPS Week 2015.

Previously:

I was at University of Illinois at Urbana Champaign for my graduate studies. My PhD thesis was supervised by Prof. Mahesh Viswanathan and Prof. Sayan Mitra. I obtained my B.Tech from Indian Institute of Technology Guwahati. I was an intern at SRI International in the Computer Science Laboratory in Summer 2012 and at NEC Labs America in the System Analysis and Verification Group in Summer 2011, and at Verimag in the Timed and Hybrid Systems Group under the supervision of Dr. Oded Maler in Summer 2008.