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.

  • Software Verification at NEC Laboratories: I contributed to the F-Soft and Varvel projects at NEC laboratories. This effort led to a state-of-the-art automatic software verification engine for C/C programs called Varvel.

  • StInG is an invariant synthesis tool that I do not maintain any longer. A successor to StInG with new and improved solution algorithms is planned sometime in 2016.

  • LPINV is a template-polyhedron abstract interpretation tool. It is no longer maintained.

Research Group

Current Members

PhD Students

Alumni

  • Dr. Xin Chen (Assistant Professor at University of Dayton, OH)

  • Hadi Ravanbakhsh (PhD in CSCI, July 2018. First Employment: Postdoctoral Researcher at University of California, Berkeley).

  • Rhys Olsen (BS in CSCI).

  • 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.

  • April 2019: Organizing SNR 2019 with Sadegh Soudjani and attending CPSWeek 2019 in Montreal, Canada. Souradeep will be presenting our paper on neural network verification at the special session on Safe AI at HSCC 2019.

  • March 2019: At Berkeley, CA for the Design of Robotics and Embedded systems, Analysis, and Modeling Seminar (DREAMS) seminar.

  • January 2019: Teaching Programming Languages to the undergraduates and algorithms to the graduate students.

  • August 2018: Papers accepted to autonomous robotics journal, and formal methods in systems design journal. Congratulations to students involved: Hadi and Jessica.

  • July 2018: Congratulations to Dr. Hadi Ravanbakhsh for successfully defending his thesis.

  • June 2018: Attending Mathworks symposium in Boston. Presenting our work on data driven models at the NAASS conference in Santa Fe, NM. Congratulations to Hadi and Sina on new IROS paper. Congratulations to Souradeep and Taisa for their CMSB paper.

  • April 2018: Congratulations to Souradeep for papers that will appear in NFM and ADHS.

  • March 2018: SANER 2018 paper wins IEEE TCSE distinguished paper award.

  • March 2018: Visiting UBC in Vancouver for a seminar on our control Lyapunov function synthesis work.