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.

  • Automotive Systems: collaboration with Toyota Technical Center (TTC).

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.

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

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

Projects (Past)

  • 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

MS Students

  • Hansol Yoon.

Undergraduate Students

  • Alex Singh (CMU, summer REU student).

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)

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

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

  • December 2017: Congratulations to Rhys and Sergio for SANER 2018 paper. Congratulations to Taisa for her papers that will appear in ATTD and ICCPS 2018.

  • November 2017: Presenting RTSS 2017 paper with Xin.

  • October 2017: EMSOFT 2017 paper with Sergio and Xin nominated for best paper award.

  • August 2017: Joint keynote talk for NSAD and TAPAS 2017 titled ‘‘static analysis of programs with probabilities’’.

  • July 2017: Congratulations to Amin Ben Sassi for the SAS 2017 paper, Xin Chen and Sergio Mover for the paper to appear in EMSOFT 2017 and Xin Chen for his RTSS 2017 paper.

  • June 2017: Congratulations to Chou Yi on her NSV workshop paper and Hadi Ravanbakhsh on the SYNT 2017 workshop paper.

  • May 2017: Congratulations to Rhys Olsen and Alexandra Okeson for graduating. Alex won the outstanding graduate award from our college. Rhys successfully defended his dissertation on testing the ‘‘popular is beautiful’’ hypothesis through statistical analysis graphs arising from large code corpuses.

  • May 2017: Congratulations to Hadi Ravanbakhsh for his RSS 2017 paper.

  • May 2017: We will be participating in the AFRL Summer of Innovation Program in Dayton, OH. Xin Chen will be leading our team on site at Dayton, OH.