Publications

Thesis

Goran Frehse. Compositional Verification of Hybrid Systems using Simulation Relations. PhD thesis, Radboud Universiteit Nijmegen, October 10, 2005. pdf

Goran Frehse. Scalable Verification of Hybrid Systems. Habilitation thesis, University Grenoble Alpes, May 26, 2016. pdf

Volumes

M. Althoff, G. Frehse, editors. ARCH20. Proceedings of 7th International Workshop on Applied Verification of Continuous and Hybrid Systems, EPiC Series in Computing, Volume 74, 2020, 274 pages

M. Althoff, G. Frehse, editors. ARCH19. Proceedings of 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, EPiC Series in Computing, Volume 61, 2019, 219 pages

M. Althoff, G. Frehse, editors. ARCH18. Proceedings of 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, EPiC Series in Computing, Volume 54, 2018, 250 pages

G. Frehse, S. Mitra, editors. Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18-20, 2017. ACM 2017

M. Althoff, G. Frehse, editors. ARCH17. Proceedings of 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, EPiC Series in Computing, Volume 48, 2017, 180 pages

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

Étienne André, Goran Frehse, editors. Proceedings of the 2nd International Workshop on Synthesis of Complex Parameters, SynCoP 2015, April 11, 2015, London, United Kingdom. OASICS 44, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015

M. Althoff, G. Frehse, editors. Post-Proceedings of the 1st and 2nd International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH’14 & ARCH’15, EPiC Series in Computing, Volume 34, 2015, 212 pages

Étienne André, Goran Frehse, editors. Proceedings of the 1st International Workshop on Synthesis of Continuous Parameters, SynCoP 2014, Grenoble, France, 6th April 2014. EPTCS 145, 2014

Sebastian Engell, Goran Frehse and Eckehard Schnieder (Eds), Modelling, Analysis and Design of Hybrid Systems, volume 279 of Lecture Notes in Control and Information Sciences. Springer-Verlag, 2002.

Book Chapters

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

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

Goran Frehse. Tools for the verification of linear hybrid automata models. In J. Lunze, F. Lamnabhi-Lagarrigue, editors, Handbook of Hybrid Systems Control, Theory – Tools – Applications, Cambridge University Press, Cambridge, 2009.

Thao Dang, Goran Frehse, Antoine Girard, Colas Le Guernic. Tools for the Analysis of Hybrid Models. In Claude Jard and Olivier (H.) Roux, editors. Communicating Embedded Systems - Software and Design. ISTE Publishing/John Wiley, October 2009

Thao Dang, Goran Frehse, Antoine Girard, Colas Le Guernic. Outils pour l'analyse des modèles hybrides. In Olivier Roux, Claude Jard, editors, Approches formelles des systèmes embarqués communicants (Traité IC2, série Informatique et systèmes d'information), Hermes Lavoisier, 2008.

Ralf Huuck, Ben Lukoschus, Goran Frehse and Sebastian Engell. Compositional verification of continuous-discrete systems. In Sebastian Engell, Goran Frehse and Eckehard Schnieder, editors, Modelling, Analysis and Design of Hybrid Systems, volume 279 of Lecture Notes in Control and Information Sciences, pages 225-244. Springer-Verlag, 2002.

Gero Nenninger, Goran Frehse and Volker Krebs. Reachability Analysis and Control of a Special Class of Hybrid Systems. In Sebastian Engell, Goran Frehse and Eckehard Schnieder, editors, Modelling, Analysis and Design of Hybrid Systems, volume 279 of Lecture Notes in Control and Information Sciences, pages 173-192. Springer-Verlag, 2002. pdf

Journal Articles

S. Bogomolov, M. Forets, G. Frehse, A. Podelski, C. Schilling, Decomposing Reach Set Computations with Low-dimensional Sets and High-dimensional Matrices (extended version), Information and Computation, 2022, 104937,

M. Althoff, G. Frehse, A. Girard. Set Propagation Techniques for Reachability Analysis. Annual Review of Control, Robotics, and Autonomous Systems, 2021, 4:1

S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling. Reachability analysis of linear hybrid systems via block decomposition. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(11): 4018-4029 (2020)

Antonio A. Bruto da Costa, Goran Frehse, Pallab Dasgupta. Formal Feature Interpretation of Hybrid Systems. IEEE Transactions on CAD, 2018.

Sergiy Bogomolov, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T. Johnson, Hamed Ladan, Andreas Podelski and Martin Wehrle. Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions, International Journal on Software Tools for Technology Transfer (STTT), 18(4): 449-467 (2016)

Goran Frehse. PHAVer: Algorithmic Verification of Hybrid Systems past HyTech. International Journal on Software Tools for Technology Transfer (STTT), Volume 10, Number 3, June, 2008. pdf BibTeX A preliminary version appeared in Manfred Morari and Lothar Thiele, editors, Hybrid Systems: Computation and Control (HSCC'05), volume 3414 of Lecture Notes in Computer Science, pages 258-273, Springer-Verlag, 2005. (revised) pdf, BibTeX (DBLP) © 2005, 2008 Springer

Conference Proceedings

S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling. Reachability analysis of linear hybrid systems via block decomposition, EMSOFT 2020 (nominated for best paper award) . pdf

S. Bogomolov, G. Frehse, A. Gurung, D. Li, G. Martius, R. Ray. Falsification of hybrid systems using symbolic reachability and trajectory splicing, HSCC, 2019. pdf

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

N. Kekatos, M. Forets, G. Frehse, Constructing Verification Models of Nonlinear Simulink Systems via Syntactic Hybridization. In Proc. IEEE Conf. Decision and Control (CDC), 2017. pdf

S. Bogomolov, G. Frehse, M. Giacobbe, T. Henzinger. Counterexample-guided refinement of template polyhedra. TACAS'17, 2017. pdf

M. Althoff and G. Frehse. Combining zonotopes and support functions for efficient reachability analysis of linear systems. In Proc. of the 55th IEEE Conference on Decision and Control, 2016. pdf

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. pdf

S. Minopoli, G. Frehse. SL2SX Translator: From Simulink to SpaceEx Verification Tool (Tool Paper). HSCC'16, ACM, 2016. pdf

G. Frehse, Computing Maximizer Trajectories of Affine Dynamics for Reachability. CDC'15. pdf

G. Frehse. Reachability of Hybrid Systems in Space-Time. Emsoft’15. pdf

G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, A. Podelski. Eliminating Spurious Transitions in Reachability with Support Functions. HSCC’15. pdf

S. Bogomolov, G. Frehse, M. Greitschus, R. Grosu, C. Pasareanu, A. Podelski and T. Strump. Assume-Guarantee Abstraction Refinement Meets Hybrid Systems. HVC'14. supplementary material

Goran Frehse, Arne Hamann, Sophie Quinton, Matthias Woehrle. Formal analysis of timing effects on closed-loop properties of control software. RTSS'14. pdf

Stefano Minopoli, Goran Frehse: Non-convex Invariants and Urgency Conditions on Linear Hybrid Automata. FORMATS'14. pdf

Alexandre Donzé, Goran Frehse. Modular, hierarchical models of control systems in SpaceEx. ECC'13. pdf

Goran Frehse, Colas Le Guernic and Rajat Kateja. Flowpipe Approximation and Clustering in Space-Time. HSCC’13. pdf

Sergiy Bogomolov, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T. Johnson, Hamed Ladan, Andreas Podelski, and Martin Wehrle. Abstraction-Based Guided Search for Hybrid Systems. SPIN’13. pdf

Goran Frehse, Rajarshi Ray. Flowpipe-Guard Intersection for Reachability Computations with Support Functions. ADHS'12. pdf

Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski and Martin Wehrle. A Box-based Distance between Regions for Guiding the Reachability Analysis of SpaceEx. CAV'12. pdf

Chen, Xin, Ábrahám, Erika, Frehse, Goran. Efficient Bounded Reachability Computation for Rectangular Automata. RP'11

Goran Frehse, Kim G. Larsen, Marius Mikucionis, Brian Nielsen. Monitoring Dynamical SIgnals while Testing Timed Aspects of a System. ICTSS'11

Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, Oded Maler. SpaceEx: Scalable Verification of Hybrid Systems. CAV'11 pdf

Goran Frehse, Rajarshi Ray. Design Principles for an Extendable Verification Tool for Hybrid Systems. ADHS'09. pdf

Goran Frehse, Sumit Kumar Jha, and Bruce H. Krogh. A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata. HSCC'08. pdf

Goran Frehse. On Timed Simulation Relations for Hybrid Systems and Compositionality. FORMATS'06. pdf

E. Asarin, T. Dang, G. Frehse, A. Girard, C. Le Guernic, O. Maler. Recent Progress in Continuous and Hybrid Reachability Analysis. CACSD'06. pdf

Goran Frehse, Bruce H. Krogh, Rob A. Rutenbar. Verifying Analog Oscillator Circuits Using Forward/Backward Abstraction Refinement. DATE'06. pdf

Goran Frehse, Zhi Han, Bruce Krogh. Assume-Guarantee Reasoning for Hybrid I/O-Automata by Over-Approximation of Continuous Interaction. CDC'04. pdf

Goran Frehse. Compositional Verification of Hybrid Systems with Discrete Interaction using Simulation Relations. CACSD'04. pdf

Goran Frehse, Olaf Stursberg, Sebastian Engell, Ralf Huuck, and Ben Lukoschus. Modular analysis of discrete controllers for distributed hybrid systems. IFAC World Congress'02.

Goran F. Frehse, Olaf Stursberg, Sebastian Engell, Ralf Huuck and Ben Lukoschus. Verification of hybrid controlled processing systems based on decomposition and deduction. ISIC'01.

G. Nenninger, G. Frehse and V. Krebs. Hybrid Regions of Attraction of Piecewise Affine Hybrid Systems. ADPM'00. pdf

G. Frehse and A. Paice. Optimal Control of a Gas Compressor Field. MTNS'00.

Workshops and Nonpublic Conferences

Hitashyam Maka, Goran Frehse, Bruce H. Krogh. Polyhedral Domains and Widening for Verification of Numerical Programs. In NSV-II: Second International Workshop on Numerical Software Verification, 2009.

Goran Frehse, Bruce H. Krogh, Rob A. Rutenbar. Verification of Hybrid Systems Using Iterative Refinement. In Semiconductor Research Corporation TECHCON 2005, Portland, USA, October 24-26, 2005.

Goran Frehse, Bruce H. Krogh, Rob A. Rutenbar, Oded Maler. Time Domain Verification of Oscillator Circuit Properties. In Workshop on Formal Verification of Analog Circuits, Edinburgh, Scotland, April 2-10, 2005.

Goran Frehse. Solving simulation relations of timed automata for the design and verification of timed discrete controllers. In RT-TOOLS 2002: Second Workshop on Real-Time Tools, Copenhagen, Denmark, August 1, 2002, 2002.

Goran Frehse. Integrated algorithmic and deductive verification of distributed control systems for hybrid processes. In MOVEP’02: Summer School on Modelling and Verification of Parallel Processes, Nantes, France, June 19-23, 2002, 2002.