Goran Frehse
Associate Professor (Maître de Conférences HdR)
Hybrid Systems Group of Oded Maler
goran dot frehse squigglything imag dot 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

    • N. Kekatos, M. Forets, G. Frehse. Constructing Verification Models of Nonlinear Simulink Models via Hybridization. CDC'17, 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'17, 2017
    • M. Althoff, G. Frehse, editors, ARCH16. Proceedings of 3rd International Workshop on Applied Verification of Continuous and Hybrid Systems, EPiC Series in Computing, Volume 43, 2017, 143 pages
    • M. Althoff and G. Frehse. Combining zonotopes and support functions for efficient reachability analysis of linear systems. CDC'16, 2016
    • A. Bruto da Costa, P. Dasgupta, G. Frehse. Formal feature analysis of hybrid automata. MEMOCODE'16, ACM/IEEE, 2016
    • S. Minopoli, G. Frehse. From Simulation Models to Hybrid Automata Using Urgency and Relaxation. HSCC'16, ACM, 2016 
    • S. Minopoli, G. Frehse. SL2SX Translator: From Simulink to SpaceEx Verification Tool (Tool Paper). HSCC'16, ACM, 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'15
    • G. Frehse. Reachability of Hybrid Systems in Space-Time. Emsoft’15
    • G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, A. Podelski. Eliminating Spurious Transitions in Reachability with Support Functions. HSCC’15
    • Alexandre Donzé, Goran Frehse. Modular, hierarchical models of control systems in SpaceEx. ECC'13
    • Goran Frehse, Colas Le Guernic and Rajat Kateja. Flowpipe Approximation and Clustering in Space-Time. HSCC’13


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



    • 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