Sriram Sankaranarayanan: Research
My primary interests lie in the computational analysis of
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:
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.
Probabilistic Program Verification project is an ongoing 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.
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
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.
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.
Post-Doctoral Research Associates
Hadi Ravanbakhsh (PhD student, CSCI).
Souradeep Dutta (PhD student, ECEE).
Tobias Leth (Visiting PhD student for Fall 2016 from Aalborg University, Denmark).
Alexandra Okeson (CSCI)
Rhys Olsen (CSCI)
Aditya Zutshi (PhD in ECEE, December 2016. First Employment: Postdoctoral Researcher at Duke University).
Aleksandar Chakarov (PhD in CS, December 2016).
Suhas Akshar Kumar (MS in ECEE 2016, First Employment: Schneider Electric).
Dr. Amin Ben Sassi (Jan 2014 - 2016. Researcher at TU Vienna).
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, PhD student at NYU).
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)
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).
A lazily updated list of events in my group. Also see CUPLV group news.
December 2015: Two papers will appear in TACAS 2016 (Eindhoven, Netherlands) and one paper in HSCC 2016 (Vienna, Austria). Congratulations Aditya, Aleks and Vris.
October 2015: Dr. Xin Chen joins us at University of Colorado, Boulder. Dr. Chen finished his PhD in computer science from RWTH Aachen University, Aachen, Germany. Dr. Chen is well-known as the developer of Flow*, a tool for constructing flowpipes of hybrid systems.