## Project Page for NSF CAREER: Automatic Analysis of Cyber Physical SystemsThis page summarizes the publications, theses, software and personnel for the NSF Award # 0953941 CAREER: Automatic Analysis of Cyber Physical Systems: Bridging the Gap between Research and Industrial Practice (March 1, 2010 - Feb 28, 2016). PI: Sankaranarayanan. ## Project GoalsThe major research goal of this project is to develop new formal verification techniques for cyber-physical systems that bridge the gap between the capabilities of existing verification algorithms, and the capabilities that an industrial strength approach requires. In particular, we focus on three major themes: Focus on reasoning about non-linear systems, bridging the gap between the current approaches focused mostly on linear hybrid systems and common industry benchmarks that require the ability to reason about non-linear systems. Focus on reasoning about the numerical issues in controllers which are typically implemented in fixed/floating points. Focus on developing tools for models that are closer to formalisms employed in the industry rather than the hybrid automaton.
Finally, the project's major educational goal is to develop courses that will bridge the gap between existing CS curriculum and the need for engineers who are trained in the fundamentals of cyber-physical systems including ideas from optimization, dynamical systems, modeling & simulation, and control theory. ## Publications (Total = 24)Note: all publications other than invited papers are peer-reviewed. Pierre Roux, Yuen-Lam Voronin, and Sriram Sankaranarayanan, Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants In Static Analysis Symposium (SAS), Volume 9837 of Lecture Notes in Computer Science pp. TBA (2016). Note: To Appear Sept. 2016
Hadi Ravanbakhsh, and Sriram Sankaranarayanan, Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework In ACM/IEEE Conference on Embedded Software (EMSOFT), pp. TBA (2016). Note: To Appear (Oct 2016)
Sriram Sankaranarayanan, Change of Basis Abstractions for Non-Linear Hybrid Systems In Nonlinear Analysis: Hybrid Systems Vol. 19, pp. 107-133 (2016).
## 2015 (2) Hadi Ravanbakhsh, and Sriram Sankaranarayanan, Counter-Example Guided Synthesis of Control Lyapunov Functions For Switched Systems In IEEE Control and Decision Conference (CDC), pp. 4232-4239 (2015).
Mohamed Amin Ben Sassi, Sriram Sankaranarayanan, Xin Chen, and Erika Abraham, Linear Relaxations of Polynomial Positivity for Polynomial Lyapunov Function Synthesis In IMA Journal of Mathematical Control and Information Vol. dnv003, pp. 39 (2015).
## 2014 (5) Hadi Ravanbakhsh, and Sriram Sankaranarayanan, Infinite Horizon Safety Controller Synthesis through Disjunctive Polyhedral Abstract Interpretation In Intl. Conference on Embedded Software (EMSOFT), pp. 15:1-15:10 (2014).
Mohamed Amin Ben Sassi, Antoine Girard, and Sriram Sankaranarayanan, Iterative Computation of Polyhedral Invariants Sets for Polynomial Dynamical Systems In IEEE Conference on Decision and Control (CDC), pp. 6348-6353 (2014).
Xin Chen, Sriram Sankaranarayanan, and Erika Abraham, Under-approximate Flowpipes for Non-linear Continuous Systems In Formal Methods in Computer-Aided Design (FMCAD), pp. 59-66 (2014).
Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy Deshmukh, and James Kapinski, Multiple-Shooting CEGAR-based falsification for hybrid systems In Intl. Conference on Embedded Software (EMSOFT), pp. 5:1 - 5:10 (2014). Note: Winner of EMSOFT 2015 Best Paper Award
Eric Goubault, Jacques-Henri Jourdan, Sylvie Putot, and Sriram Sankaranarayanan, Finding Non-Polynomial Positive Invariants and Lyapunov Functions for Polynomial Systems through Darboux Polynomials In Proc. American Control Conference (ACC), pp. 3571 - 3578 (2014).
## 2013 (6)Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy Deshmukh, and James Kapinski, A trajectory splicing approach to concretizing counterexamples for hybrid systems In IEEE Conference on Decision and Control (CDC) pp. 3918-3925 (2013), IEEE Press.
Sriram Sankaranarayanan, Xin Chen, and Erika Abraham, Lyapunov Function Synthesis Using Handelman Representations In IFAC conference on Nonlinear Control Systems (NOLCOS) pp. 576-581 (2013).
Swarat Chaudhuri, Sriram Sankaranarayanan, and Moshe Vardi, Regular Real Analysis In IEEE Symposium on Logic in Computer Science (LICS) pp. 509-518 (2013), IEEE Press.
Aleksandar Chakarov, and Sriram Sankaranarayanan, Probabilistic Program Analysis using Martingales In Computer-Aided Verification (CAV) Volume 8044 of Lecture Notes in Computer Science, pp. 511-526 (2013), Springer-Verlag.
Xin Chen, Erika Abraham, and Sriram Sankaranarayanan, Flow*: An Analyzer for Non-Linear Hybrid Systems In Computer-Aided Verification (CAV) Volume 8044 of Lecture Notes in Computer Science, pp. 258-263 (2013), Springer-Verlag.
Sriram Sankaranarayanan, Aleksandar Chakarov, and Sumit Gulwani, Static Analysis for Probabilistic Programs: Inferring Whole Program Properties from Finitely Many Paths In ACM conference on Programming Languages Design and Implementation (PLDI) pp. 447-458 (2013), ACM Press.
## 2012 (5)Xin Chen, Erika Abraham, and Sriram Sankaranarayanan, Taylor Model Flowpipe Construction for Non-linear Hybrid Systems In Real Time Systems Symposium (RTSS) pp. 183-192 (2012), IEEE Press.
Arlen Cox, Sriram Sankaranarayanan, and Bor-Yuh Evan Chang, A Bit too Precise? Bounded Verification of Quantized Digital Filters In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Volume 7214 of Lecture Notes in Computer Science, pp. 33-42 (2012).
Aditya Zutshi, Sriram Sankaranarayanan, and Ashish Tiwari, Timed Relational Abstractions for Sampled Data Control Systems In Computer-Aided Verification (CAV) Volume 7358 of Lecture Notes in Computer Science, pp. 343-361 (2012), Springer-Verlag.
Alejandro Sanchez, Sriram Sankaranarayanan, Cesar Sanchez, and Bor-Yuh Evan Chang, Invariant Generation for Parametrized Systems using Self-Reflection In Static Analysis Symposium (SAS) Volume 7460 of Lecture Notes in Computer Science, pp. 146-163 (2012), Springer-Verlag.
Yan Zhang, Sriram Sankaranarayanan, and Fabio Somenzi, Piecewise linear modeling of nonlinear devices for formal
verification of analog circuits In Formal Methods in Computer-Aided Design ( FMCAD 2012 ) pp. 196-203 (2012), IEEE Press.
## 2011 (3)Sriram Sankaranarayanan, and Ashish Tiwari, Relational Abstractions for Continuous and Hybrid Systems In Computer-Aided Verification (CAV) Volume 6806 of Lecture Notes in Computer Science, pp. 686-702 (2011), Springer-Verlag.
Michael Colon, and Sriram Sankaranarayanan, Generalizing the Template Polyhedral Domain In European Symposium on Programming (ESOP) Volume 6602 of Lecture Notes in Computer Science, pp. 176-195 (2011), Springer-Verlag.
Sriram Sankaranarayanan, Automatic Abstraction of Non-Linear Systems Using Change of Variables Transformations In Hybrid Systems: Computation and Control (HSCC) pp. 143-152 (2011), ACM Press.
## ThesesAleksandar Chakarov, Deductive Techniques for Probabilistic Program Analysis, PhD Thesis (July 2016, expected).
## PersonnelSriram Sankaranarayanan (PI). Aleksandar Chakarov (PhD, CSCI). Hadi Ravanbakhsh (PhD, CSCI). Yuen-Lam Voronin (Postdoctoral research associate, CSCI). Xin Chen (Postdoctoral research associate, CSCI).
## PastYan Zhang (PhD, ECEE) Mohamed Amin Ben Sassi (Postdoctoral research associate, CSCI)
## CollaboratorsDr. Erika Abraham (RWTH Aachen University). Profs. Eric Goubault and Sylvie Putot (Ecole Polytechnique, France). Dr. Pierre Roux (Onera, France).
## SoftwareThe Flow* tool is available online. ## UpcomingPolynomial Optimization Solver using Bernstein polynomials. |