Goran Frehse

Associate Professor, Hybrid Systems Semantics group, Computer Science and System Engineering Laboratory (U2IS)

goranf squigglything gmail.com, @GoranFrehse, ORCiD ID

Office R.2.23 (getting here)

ENSTA Paris, U2IS; 828, boulevard des maréchaux; 91762 Palaiseau Cedex, France

Phone: +33 18 187 2076

Workshops and Conferences

Recent and Selected Publications DBLP, Google Scholar

  • S. Bogomolov, G. Frehse, A. Gurung, D. Li, G. Martius, R. Ray. Falsification of hybrid systems using symbolic reachability and trajectory splicing, HSCC, 2019
  • S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling. JuliaReach: a toolbox for set-based reachability. (Tool Paper) HSCC, 2019
  • Antonio A. Bruto da Costa, Goran Frehse, Pallab Dasgupta. Formal Feature Interpretation of Hybrid Systems. IEEE Transactions on CAD, 2018.
  • Goran Frehse, Mirco Giacobbe and Thomas Henzinger. Spacetime Interpolants. CAV, 2018. pdf
  • G. Frehse, N. Kekatos, D. Nickovic, J. Oehlerking, S. Schuler, A. Walsch, M. Woehrle. Pattern Templates and Monitors for Verifying Safety Properties of Hybrid Automata. In Proc. American Control Conference (ACC), 2018. pdf
  • S. Bogomolov, M. Forets, G. Frehse, A. Podelski, C. Schilling, F. Viry. Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices. HSCC, 2018. pdf
  • L. Doyen, G. Frehse, G. Pappas, A. Platzer. Verification of Hybrid Systems. In E.M. Clarke, T.A. Henzinger, H. Veith, editors, Handbook of Model Checking, Springer, 2018
  • N. Kekatos, M. Forets, G. Frehse. Constructing Verification Models of Nonlinear Simulink Models via Hybridization. CDC, 2017. pdf
  • S. Bogomolov, G. Frehse, M. Giacobbe, T. Henzinger. Counterexample-guided refinement of template polyhedra. TACAS, 2017. pdf
  • G. Frehse. An Introduction to Hybrid Automata, Numerical Simulation and Reachability Analysis. In R. Drechsler, U. Kühne, editors, Formal Modeling and Verification of Cyber-Physical Systems, 1st International Summer School on Methods and Tools for the Design of Digital Systems, Springer, 2015. pdf
  • G. Frehse. Reachability of Hybrid Systems in Space-Time. Emsoft, 2015. pdf


  • SpaceEx is a tool platform for algorithms related to reachability and safety verification.
  • PHAVer is a tool for formally verifying safety properties of hybrid systems with simple dynamics.



  • Industrial collaboration project with DENSO Automotive Deutschland: A Modeling, Identification and Verification Framework for Control Design in Large-Scale and Complex Systems (2017-2018)
  • IPL Modeliscale (2017-2021) is a French research collaboration project financed by INRIA
  • UnCoVerCPS (2015-2018) is a European research project investigating the integration of verification techniques in the control of cyber-physical systems
  • Multiform (2008-2012) was a European research project aiming to improve coherent tool support for the integrated control design of large and complex networked systems



  • HSCC: Conference on Hybrid Systems: Computation and Control
  • FORMATS: Conference on Formal Modeling and Analysis of Timed Systems
  • CAV: Conference on Computer Aided Verification