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

Post-Doctoral Research Associates

PhD Students

  • Hadi Ravanbakhsh (PhD student, CSCI).

  • Souradeep Dutta (PhD student, ECEE).

  • Tobias Leth (Visiting PhD student for Fall 2016 from Aalborg University, Denmark).

MS Students

  • Dimitrios Economou (CSCI)

  • Ram Das Diwakaran (CSCI)

  • Yi Chou (CSCI)

Undergraduate Students

  • Alexandra Okeson (CSCI)

  • Rhys Olsen (CSCI)

Alumni

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

News

A lazily updated list of events in my group. Also see CUPLV group news.

  • November 2016: Colloquium on our artificial pancreas work at Stanford University.

  • November 2016: Invited talk at SETTA 2016 in Beijing, China.

  • October 2016: Poster at CPS PI meeting in Washington, D.C.

  • August 2016: Welcome Souradeep Dutta, who joins our group as a PhD student.

  • August 2016: Prof. Oded Maler from Verimag, France will be visiting our group.

  • July 2016: Congratulations Dr. Aleksandar Chakarov and Dr. Aditya Zutshi for successfully defending their respective PhD theses.

  • June 2016: Paper on verified semi-definite programming co-authored with Pierre and Vris will appear in SAS’16. Congratulations to Pierre and Vris.

  • May 2016: Hadi Ravanbakhsh's paper on robust synthesis for reach-while-stay properties accepted at EMSOFT’16. Congratulations, Hadi!

  • April 2016: Presenting our medical devices work at the NSF sponsored Cyber Cardia project workshop at Stony Brook, NY.

  • April 2016: Aditya Zutshi won the HSCC 2016 best paper award sponsored by DENSO for his work on symbolic numeric reachability at HSCC 2016 in Vienna. Congratulations, Aditya!

  • April 2016: Aleks Chakarov presenting two of our papers on probabilistic systems at TACAS 2016 in Eindhoven.

  • February 2016: CPS Seminar at the University of Southern California.

  • January 2016: Teaching a seminar on closed loop medical devices in Spring 2016. Class will meet for an hour each week Wednesdays. More details coming soon.

  • December 2015: Two papers will appear in TACAS 2016 (Eindhoven, Netherlands) and one paper in HSCC 2016 (Vienna, Austria). Congratulations Aditya, Aleks and Vris.

  • December 2015: Aditya Zutshi successfully defends his PhD proposal. Congratulations, Aditya!

  • December 2015: Fearless Friday Talk about artificial pancreas research to undergraduate students and faculty in the mathematics/computer science department at Colorado College.

  • November 2015: Amin Ben Sassi will be talking about research on Bernstein polynomials and nonlinear optimization at TU Vienna, Austria.

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

  • September 2015: Hadi Ravanbakhsh's paper accepted to CDC 2015. Congratulations, Hadi!

  • September 2015: Invited Talk at Runtime Verification (RV) 2015 on the Artificial Pancreas research project.

  • September 2015: Co-Chairing FORMATS 2015 with Prof. Enrico Vicario.

  • September 2015: Aditya Zutshi presenting our work on simulation-based falsification in American Control Conference (ACC) 2015.

  • June 2015: Presenting our work on bilinear optimization and numerical abstract interpretation at the VORACE meeting in Toulouse, France.

  • April 2015: Co-Chairing HSCC 2015 with Prof. Antoine Girard.