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.