Symbolic Verification of Hybrid Systems

This is a project page for  an ongoing NSF funded effort at the CPS Verification Research Group at CU Boulder. The overall goal of this project is to develop tools and techniques for verifying hybrid, Cyber-Physical Systems that model discrete systems (programs) interacting with a continuous world (physical systems). There are three major focus areas for this project

  • With hybrid automata theory as a basis, the project seeks to develop a verification framework operating on  more realistic models of hybrid systems that incorporate complex software systems and non-linear physical environments.
  • Develop fundamental approaches to deal with the challenges of non-linear dynamics in the physical system models and richer features in the software system including lookup tables, non-linear functions and so on.
  • Build tools and benchmark suites to test the effectiveness of our approaches.
  • Analysis of floating point errors and the broader problem of robustness to various errors: quantization, timing jitters, sensor/actuator noise,…



Project Team


Principal Investigator: Prof. Sriram Sankaranarayanan.




st of students who have contributed at various stages of our project.

  • Aditya Zutshi (PhD, ECEE)
  • Yan Zhang (PhD, ECEE)
  • Arlen Cox (PhD, ECEE)
  • Aleksandar Chakarov (PhD, CS)
  • Hadi Ravanbakhsh (PhD, CS)



i>Prof. Erika Abraham and Xin Chen (RWTH, Aachen University, Germany).
  • Dr. Michael Colon (Naval Research Labs, Washington, D.C., USA).
  •  Drs. Eric Goubault and Sylvie Putot (CEA-List, Saclay, France).
  •  Drs. Franjo Ivancic and Aarti Gupta (NEC Laboratories America, Princeton, NJ, USA).
  •  Dr. Ashish Tiwari (SRI, Menlo Park, USA)
  • Publica



    •  Talk at Col


      CS+Maths Colloquium, Nov 2011. PDF
    •  Invited Talk at Workshop on Automata Theory and Applications at Inst. of Mathematical Sciences, National University of Singapore (NUS), Sept. 2011.
    •  Applied Mathematics Colloquium on Algebraic Verification of Hybrid Systems at CU-Boulder, Oct. 2010  PDF
    •  Talk at Midwest Verification Day on Algebraic Verification of Hybrid Systems, August 2010 (Cf. applied maths colloquium for latest slides).
    •  Talk on linearizing abstractions for non-linear systems at Academia Polyhedrica, Colorado State University, July 2010.
    •  Talk on Algebraic Verification of Hybrid Systems at HSCC 2010, Copenhagen, Sweden, Apr. 2010.


    We are releasing cod


    aterials as part of our efforts.



    This research  has been sponsor

    al Science Foundation (NSF) CAREER Award # 0953941. All opinions expressed here are those of the author and not necessarily those of the US National Science Foundation or the University of Colorado, Boulder.