Goran Frehse
Professor (Enseignant Chercheur HdR)
Hybrid Systems Semantics group
Computer Science and System Engineering Laboratory (U2IS)
goranf squigglything gmail.com
@GoranFrehse, ORCiD ID
Office R223

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

Phone: +33 18 187 2076

Workshops and Conferences

    Recent and Selected Publications DBLPGoogle Scholar

    • 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
    • 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
    • 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
    • M. Althoff and G. Frehse. Combining zonotopes and support functions for efficient reachability analysis of linear systems. CDC, 2016. pdf
    • A. Bruto da Costa, P. Dasgupta, G. Frehse. Formal feature analysis of hybrid automata. MEMOCODE, ACM/IEEE, 2016
    • 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, Computing Maximizer Trajectories of Affine Dynamics for Reachability. CDC, 2015. pdf
    • G. Frehse. Reachability of Hybrid Systems in Space-Time. Emsoft, 2015. pdf
    • Alexandre Donzé, Goran Frehse. Modular, hierarchical models of control systems in SpaceEx. ECC, 2013pdf
    • Goran Frehse, Colas Le Guernic and Rajat Kateja. Flowpipe Approximation and Clustering in Space-Time. HSCC, 2013. 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



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