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
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
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,
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)
Abstractions for Hybrid Systems Verification
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 Automata, Black-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.
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.
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: https://uofi.app.box.com/v/HARE