Goran Frehse
Associate Professor (Maître de Conférences HdR)
Hybrid Systems Group of Oded Maler
goran dot frehse squigglything univ-grenoble-alpes.fr

Laboratoire Verimag - Bâtiment IMAG, office 207
Université Grenoble Alpes
700 avenue centrale

38401 Saint-Martin-d’Hères, France
Phone: +33 4 57 42 22 16

Postal address:
Laboratoire Verimag - Bâtiment IMAG
Université Grenoble Alpes
CS 40700
38058 GRENOBLE CEDEX 9, France

Workshops and Conferences

    Recent and Selected Publications DBLPGoogle Scholar

    • 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 (to appear)
    • 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 (to appear)
    • N. Kekatos, M. Forets, G. Frehse. Constructing Verification Models of Nonlinear Simulink Models via Hybridization. CDC, 2017
    • 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 (to appear)
    • S. Bogomolov, G. Frehse, M. Giacobbe, T. Henzinger. Counterexample-guided refinement of template polyhedra. TACAS, 2017
    • M. Althoff and G. Frehse. Combining zonotopes and support functions for efficient reachability analysis of linear systems. CDC, 2016
    • 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
    • G. Frehse, Computing Maximizer Trajectories of Affine Dynamics for Reachability. CDC, 2015
    • G. Frehse. Reachability of Hybrid Systems in Space-Time. Emsoft, 2015
    • Alexandre Donzé, Goran Frehse. Modular, hierarchical models of control systems in SpaceEx. ECC, 2013
    • Goran Frehse, Colas Le Guernic and Rajat Kateja. Flowpipe Approximation and Clustering in Space-Time. HSCC, 2013


    • 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