Static Analysis in the Continuously Changing World

  • Sriram Sankaranarayanan
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7935)


In this talk, we examine static analysis techniques for continuous-time dynamical systems. Continuous time systems arise in many domains including engineered control systems, physical and biological systems. They are increasingly of interest to the static analysis community, due to the focus on hybrid (cyber-physical) systems that capture discrete programs interacting with a continuous external environment. We examine two types of properties that are typically verified: reachability and stability, and explore parallels between commonly used static analysis approaches and a variety of approaches to prove/disprove reachability and stability properties.


Hybrid System Lyapunov Function Taylor Model Continuous Time System Automatic Synthesis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Asarin, E., Dang, T., Maler, O.: The d/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Chen, X., Ábrahám, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proc. RTSS 2012, pp. 183–192. IEEE (2012)Google Scholar
  3. 3.
    Chutinan, A., Krogh, B.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proceedings of IEEE CDC. IEEE Press (1998)Google Scholar
  4. 4.
    Cousot, P., Cousot, R.: Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. ACM Principles of Programming Languages, 238–252 (1977)Google Scholar
  5. 5.
    Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past hyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  7. 7.
    Henzinger, T.A., Ho, P.: HyTech: The Cornell hybrid technology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 265–293. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  8. 8.
    Lunze, J., Lamnabhi-Lagarrigue, F. (eds.): Handbook of Hybrid Systems Control: Theory, Tools and Applications. Cambridge University Press (2009)Google Scholar
  9. 9.
    Meiss, J.D.: Differential Dynamical Systems. SIAM Publishers (2007)Google Scholar
  10. 10.
    Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (1999)Google Scholar
  11. 11.
    Papachristodoulou, A., Prajna, S.: On the construction of lyapunov functions using the sum of squares decomposition. In: IEEE CDC, pp. 3482–3487. IEEE Press (2002)Google Scholar
  12. 12.
    Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143–189 (2008)MathSciNetzbMATHCrossRefGoogle Scholar
  13. 13.
    Platzer, A., Quesel, J.-D.: KeYmaera: A hybrid theorem prover for hybrid systems (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  14. 14.
    Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. 15.
    Prajna, S., Papachristodoulou, A., Seiler, P., Parrilo, P.A.: SOSTOOLS: Sum of squares optimization toolbox for MATLAB (2004)Google Scholar
  16. 16.
    Sankaranarayanan, S., Sipma, H., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods in System Design 32(1), 25–55 (2008)zbMATHCrossRefGoogle Scholar
  17. 17.
    Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer (2009)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Sriram Sankaranarayanan
    • 1
  1. 1.University of ColoradoBoulderUSA

Personalised recommendations