About me [CV]
I am an Assistant Professor at University of Connecticut
in the Department of
Computer Science and Engineering. My
research is about developing scalable approximation and
abstraction techniques for verifiying high dimensional
CPS with complex software.
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 investigating scalable dynamic analysis
techniques for verification of linear hybrid systems. My
recent 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
This work has won the Best Paper Award at ARCH
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.
- [[April 2017]] Join 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
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.
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
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
and Hybrid Systems Group under the supervision of
Maler in Summer 2008.