I am a PhD candidate at Department of Computer Science, University of Colorado-Boulder. I'm a member of CUPLV group and my advisor is Prof. Sriram Sankaranarayanan. My field of research is Formal Methods. In particular I'm interested in verification and synthesis of cyber-physical systems (systems in which computer systems interact with the physical environment). The ideal goal in these problems is to design systems which behave as expected (admit some specifications).

In 2012, I started my Ph.D. and for my thesis, I'm developing methods for automatic controller synthesis using control certificates and counterexamples. My research is supported by NSF.


  • Natural Language Processing
  • Formal Verification
  • Cyber-Physical Systems
  • Programming Languages
  • Program Analysis
  • Program Synthesis
  • Linear Programming
  • Advanced Linear Systems
  • Dynamical Systems
  • Advanced Algorithms
  • Projects

  • Modeling and Verification
           for insulin infusion pump
  • Control Synthesis for Safety
           using fixed-point computation
  • Control Synthesis for Stability
           using constraint-solving
  • Modeling and Control Design
           for ninja car

  • Publications

    Conference Papers

  • H. Ravanbakhsh and S. Sankaranarayanan, “Learning Lyapunov (Potential) Functions from Counterexamples and Demonstrations”, Robotics: Science and Systems. (RSS-2017)
  • H. Ravanbakhsh and S. Sankaranarayanan, “Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework”, Conference on Embedded Software. (EMSoft-2016)
  • H. Ravanbakhsh and S. Sankaranarayanan, “Counter-Example Guided Synthesis of Control Lyapunov Functions for Switched Systems”, IEEE Conference on Decision and Control. (CDC-2015)
  • H. Ravanbakhsh and S. Sankaranarayanan, “Infinite Horizon Safety Controller Synthesis through Disjunctive Polyhedral Abstract Interpretation”, Conference on Embedded Software. (EMSoft-2014)
  • S. Sankaranarayanan, C. Miller, R. Raghunathan, H. Ravanbakhsh and G. Fainekos, “Analyzing Insulin Infusion Pump Usage Strategies in Diabetic Patients (I)”, 50th Annual Allerton Conference on Communication, Control, and Computing. (Allerton-2012)
  • H. Faili, H. Ravanbakhsh, “Affix-Augmented Stem-Based Language Model for Persian”, In proceedings of Natural Language Processing and Knowledge Engineering (NLPKE-2010)
  • Invited Talks, Posters, Etc.

  • Workshop: “A Class of Control Certificates to Ensure Reach-While-Stay for Switched Systems” (SYNT-2017)
  • Invited Talk: “Automatic Synthesis of Controllers from Specifications using Control Certificate” (V2CPS-2016)
  • Invited Talk: “Counter-example guided inductive synthesis of controllers”, Towards Scalable Formal Synthesis of Complex Systems. (CDC-2015)
  • Technical Report: ”Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay Properties”
  • Poster: “Counterexample-guided Stabilization of Switched Systems using Control Lyapunov Functions” (HSCC-2015)
  • B.Sc. Thesis: “An Energy-Optimal Real-Time Scheduling Algorithm for Unrelated DVS-Enabled Parallel Machines”