Parasara Sridhar Duggirala

Research Group

Current Graduate Students

Abolfazal Karimi, PhD Student
Manish Goyal, PhD Student
Bineet Ghosh, PhD Student
Tao Tao, PhD Student

Undergraduate Students Mentored at UConn

Renukanandan Tumu, CSE@UConn.
Jonathan Homburg, double major in CSE & Math @UConn.

Current Research Projects

My research interests span the areas of Formal Methods, Cyber-Physical Systems, Control Theory, Numerical Methods, and Decision procedures. I am currently working on the following research themes.

Certification of Autonomous Vehicles

                  For Certifying Autonomous Vehicles
Autonomous vehicles is considered as the next major technological revolution. Companies like Google, Tesla, and Uber are already testing these autonomous vehicles on roads. Majority of the auto-manufacturers have already announced plans to develop autonomous vehicles. Several accidents regarding these autonomous vehicles are already documented and the recent crash of Tesla while running on Auto-pilot is documented as the first fatal accident.

It is therefore, very important to verify the functional correctness of an autonomous vehicle. My students and I have built a prototype autonomous vehicles for verifying not just the high-level specification, but also to verify the controllers, and the underlying real-time system. In that past, I have worked on bridging the gap between the controllers and the real-time timing delays faced by the implementation. The paper can be obtained here (ppt).

Dynamic Analysis of Cyber-Physical Systems

Dynamic analysis broadly refers to the set of techniques where a property of the underlying system is proved by examining sample behaviors of the system. A dynamic analysis technique for CPS should take into account both the continuous behaviors (governed by the physical laws) and the discrete behavior (governed by software). For CPS where the continuous behaviors are given as linear differential equations, then I have developed a technique for efficiently computing the set of reachable states. For an n-dimensional linear system, this technique requires a mere n+1 sample behaviors (paper, ppt).

Together with Stanley Bak, I have extended these techniques for hybrid systems which take into account discrete transitions. For performing such extensions, we developed two new techniques. The first being Invariant constraint propagation and the second being dynamic de-aggregation. Details about these two techniques can be obtained in this paper (ppt). We have also extended these techniques to work with piecewise-constant input signal and verify the safety property. Our technique has discovered a previously unknown safety violation of a 277 dimensional Space-Station model and we could improve the scalability of verification to 10,000 dimensions. This work has won the Best Paper Award at ARCH Workshop, 2017. The relevant paper and presentation are here (paper, paper, ppt)

Reachable Set
Invariant Constraint
Dynamic Deaggregation

Abstractions for Hybrid Systems Verification

                  Depicting Abstraction Refinement
Abstraction is a common technique used in "simplifying" a complex system into a simpler system and hence making the verification feasible. One of the drawback of the abstractions is that if the simpler system violates a certain property, one cannot infer that the original system violates the property. Hence, typical abstraction techniques have 4 steps: abstraction, verification, validation, and refinement to give the most accurate verification results. This sequence of steps is often called Abstraction-Refinement.

In the past, I have worked on computing abstractions of hybrid systems for verifying both the safety and liveness properties of hybrid systems. The papers that compute abstractions for safety verification are available here (paper, paper) and the papers that compute abstraction for liveness properties are available here (paper, paper, ppt, ppt). This paper has won the Best Paper Award at International Conference on Embedded Software (EMSOFT) 2013.

Miscellaneous projects.

In addition to the above projects, I am also interested to work on Techniques for Minimization of Symbolic AutomataBlack-Box Techniques For Falsification, and Decision Procedures Using Numerical Techniques (read Numerical Algebraic Geometry). Please send me an email if you are interested to know more about these projects.


I have been a part of the following research tools.

HyLAA (Hybrid Linear Automata Analyzer): A tool for verification of linear dynamical and hybrid systems by exploiting the superposition principle of linear dynamics using generalized stars. Also implements new techniques such as constraint propagation and aggregation techniques. Developed in collaboration with Dr. Stanley Bak of Air Force Research Laboratory.

C2E2 (Compare Execute Check Engine): A tool for safety verification of annotated Stateflow models from sample simulations. The tool is used in Universities and Research Labs such as University of Texas at Arlington, Michigan State University, Air Force Research Laboratory, and NASA.

HARE (Hybrid Abstraction Refinement Engine): A tool for performing Counter-Example Guided Abstraction Refinement (CEGAR) on rectangular hybrid automata, built on top of model checker HyTech. A new version of the tool that can perform abstraction refinement for nonlinear hybrid automata has been developed by Nima Roohi. Please refer to his work for latest developments.
New Version: