Sriram Sankaranarayanan: Research
Research Introduction
My primary interests lie in the computational analysis of
Cyber-Physical
Systems, that involve the interaction of software components inside a
physical system. Examples include software-based control systems for
automotive, avionics and medical applications. The challenges include
mathematical modeling of enviromental uncertainties, reasoning about
these mathematical models to automatically prove or falsify
correctness properties, and synthesizing core software subsystems
automatically from given correctness specifications. My research
addresses foundational (theoretical) issues including the theory of
hybrid dynamical systems as well as applications to closed-loop
medical devices and automotive systems.
I am part of the Programming Languages &
Verification and Hybrid Systems communities, a very exciting area at the intersection
of computer science and control theory. I take an active interest in
topics that are directly relevant to my research, including convex
optimization, randomized algorithms, algebraic/semi-algebraic
geometry, combinatorial optimization, monte-carlo methods, symbolic
and numerical decision procedures.
Current foundational topics of interest include:
Reachability and stability verification of hybrid dynamical systems.
Automatic approaches to falsification (counterexample generation).
Correct-by-construction synthesis of control systems.
Probabilistic program analysis/verification.
Optimization and decision problems such as guaranteed nonlinear optimization and multilinear problems.
Current applications areas of focus include:
Closed Loop Medical Systems: Artificial Pancreas collaboration with the Barbara Davis Center.
Verification of Artificially Intelligent Autonomous Systems: Collaboration with SRI, USA.
Projects (Current)
Here is a (partial) list of ongoing projects.
Artificial Pancreas Verification Project is a collaboration between
engineers, computer scientists, mathematicians, and clinical
researchers centered around the mathematical modeling, simulation
and formal analysis of the artificial pancreas concept.
Flow* constructs flowpipe approximations for
hybrid system models. Given a mathematical model of a nonlinear
hybrid dynamical system, a set of initial states and set of input
signals, the tool computes a safe overapproximation of the reachable
set of states over time. In doing so, it can isolate rare behaviors
that may not be easy to find using testing or prove that a property
is satisfied by the model.
S-Taliro is a
Matlab toolbox that searches for counter-examples to properties in
complex Cyber-Physical Systems. Given a closed-loop control system
model that can be simulated inside Matlab(tm) SimulinkStateflow
environment and a specified property of the model, S-Taliro
systematically searches for violations. To do so, it uses a notion
of robustness that measures how far away a continuous-time (or a
mixed discretecontinuous-time) signal is from violating a property
of interest.
Guaranteed nonlinear solvers project seeks the combination of
numeric and symbolic nonlinear optimization tools for solving
verification and synthesis problems. Under this project we are
investigating linear relaxations of nonlinear (polynomial) problems,
facial reduction in sum-of-squares optimization problems and
algorithms for guaranteed bilinear/multilinear feasibility problems.
All these optimization problems are central to the
verification and synthesis of Cyber-Physical Systems.
Projects (Past)
Probabilistic Program Verification project is a past NSF-funded
project wherein we are developing ideas for verifying stochastic
systems. As part of this work, we have developed techniques using
martingale theory and concentration of measure inequalities for
reasoning about programs that process uncertain (random) inputs.
S3CAM (web page and user manual
coming soon) is an explicit state model checker for black-box
models. It combines a graph-based abstraction technique with
on-the-fly explicit model checking for property violations. It is
being developed jointly in collaboration with Drs. Jyotirmoy
Deshmukh, James Kapinski and Xiaoqing Jin at Toyota motors.
Research Group
Current Members
PhD Students
Yi Chou (PhD student, CSCI).
Emily Jensen (PhD Student, CSCI).
Monal Narasimhamurthy (PhD Student, CSCI).
Kandai Watanabe (PhD Student, CSCI jointly advised with Morteza Lahijanian).
Hansol Yoon (PhD student, CSCI).
Alumni
Souradeep Dutta (PhD, ECEE, June 2020, First Employment: Postdoc at Univ. Pennsylvania.).
Taisa Kushner (PhD, IQ Biology, First Employment: Computing Innovation Fellow at Oregon Health Sciences University Medical School).
Dr. Xin Chen (Assistant Professor at University of Dayton, OH)
Hadi Ravanbakhsh (PhD in CSCI, July 2018. Employment: Google Inc.).
Rhys Olsen (BS in CSCI, Employment: Google Inc.).
Alexandra Okeson (BS in CSCI, PhD student at the University of Washington).
Dimitrios Economou (MS in CSCI)
Ram Das Diwakaran (MS in CSCI, First Employment: Texas Instruments Inc.).
Dr. Yuen-Lam (Vris) Voronin (First Employment: Tradewins Inc.).
Aditya Zutshi (PhD in ECEE, December 2016. First Employment: Postdoctoral Researcher at Duke University).
Aleksandar Chakarov (PhD in CS, December 2016. First Employment: Research Scientist at Phase Change Inc.).
Suhas Akshar Kumar (MS in ECEE 2016, First Employment: Schneider Electric).
Dr. Amin Ben Sassi (Jan 2014 - 2016. Assistant Professor at Mediterranean School of Business).
Arlen Cox (PhD in ECEE, December 2014. First Employment: IDA/CCS).
Yan Zhang (PhD in ECEE, Summer 2014. Current Employment: Huawei Research, Singapore).
Huxley Bennett (MS in CSCI 2012, Postdoc at Northwestern University).
Hadjar Homaie (MS, 2011, First Employment: Amazon).
Sidartha Gracias (MS, 2011).
Aaron Schlicht (ME, 2011).
Christopher Miller (BS, 2014, PhD student at Georgia Tech).
Paul Givens (BS, 2014, First Employment: Software Engineer at IOSemantics).
Nathan Lapinski (BS, 2014, MS student at CU Boulder).
Long Term Visitors (Past)
Arthur Claviere (Ecole Polytechnique and Supaero, France).
Alex Singh (CMU, summer REU student).
Tobias Leth (Aalborg University, Denmark).
Dr. Pierre Roux (Onera, Toulouse, France).
Xin Chen (PhD student at RWTH Aachen University, Germany).
Xue Bai (PhD, Beihang University, China. On a Chinese Student Council Fellowship).
Zuxi Chen (PhD, Tongji University, China. On a Chinese Student Council Fellowship).
News
A lazily updated list of events in my group. Also see CUPLV group news.
March 2019: At Berkeley, CA for the Design of Robotics and Embedded systems, Analysis, and Modeling Seminar (DREAMS) seminar.
|