Journal Articles

  1. Ghorbal K, Sogokon A, Platzer A (2017) A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Computer Languages, Systems & Structures 47:19–43. doi: 10.1016/j.cl.2015.11.003
    This paper studies sound proof rules for checking positive invariance of algebraic and semi-algebraic sets, that is, sets satisfying polynomial equalities and those satisfying finite boolean combinations of polynomial equalities and inequalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the trade-off between proof rule generality and practical performance and evaluate our theoretical observations on a set of benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting.
    @article{Ghorbal2017,
      author = {Ghorbal, Khalil and Sogokon, Andrew and Platzer, Andr{\'{e}}},
      title = {A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets},
      journal = {Computer Languages, Systems {\&} Structures},
      year = {2017},
      volume = {47},
      pages = {19--43},
      month = jan,
      doi = {10.1016/j.cl.2015.11.003},
      file = {:papers/comlan2016.pdf:PDF},
      keywords = {Formal Verification, Polynomial Differential Equations, Positive Invariance, Deductive Power, Dynamical Systems},
      publisher = {Elsevier {BV}},
      timestamp = {Mon, 05 Jun 2017 01:00:00 +0200},
      url = {https://doi.org/10.1016/j.cl.2015.11.003}
    }
    
  2. Jeannin J-B, Ghorbal K, Kouskoulas Y, and others (2017) A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. International Journal on Software Tools for Technology Transfer 19:717–741. doi: 10.1007/s10009-016-0434-1
    The Next-Generation Airborne Collision Avoid- ance System (ACAS X) is intended to be installed on all large aircraft to give advice to pilots and prevent mid-air collisions with other aircraft. It is currently being developed by the Federal Aviation Administration (FAA). In this paper we determine the geometric configurations under which the advice given by ACAS X is safe under a precise set of assumptions and formally verify these configurations using hybrid systems theorem proving techniques. We consider subsequent advisories and show how to adapt our formal verification to take them in to account. We examine the current version of the real ACAS X system and discuss some cases where our safety theorem conflicts with the actual advisory given by that version, demonstrating how formal hybrid systems proving approaches are helping to ensure the safety of ACAS X. Our approach is general and could also be used to identify unsafe advice issued by other collision avoidance systems or confirm their safety.
    
    @article{Jeannin2017,
      author = {Jeannin, Jean-Baptiste and Ghorbal, Khalil and Kouskoulas, Yanni and Schmidt, Aurora and Gardner, Ryan and Mitsch, Stefan and Platzer, Andr{\'{e}}},
      title = {A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system},
      journal = {International Journal on Software Tools for Technology Transfer},
      year = {2017},
      volume = {19},
      number = {6},
      pages = {717--741},
      month = oct,
      doi = {10.1007/s10009-016-0434-1},
      file = {:papers/safe_zones.pdf:PDF},
      publisher = {Springer Nature},
      timestamp = {Mon, 16 Oct 2017 01:00:00 +0200},
      url = {https://doi.org/10.1007/s10009-016-0434-1}
    }
    
  3. Martin B, Ghorbal K, Goubault E, Putot S (2017) Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System. Electronic Proceedings in Theoretical Computer Science 257:91–104. doi: 10.4204/eptcs.257.9
    In this case study paper, we investigate the formal verification of a hybrid control law designed to perform a station keeping maneuver for a planar vehicle. Such maneuver requires that the vehicle reaches a neighborhood of its station in finite time and remains in it while waiting for further commands. We model the dynamics as well as the control law as a hybrid program and formally verify the reachability and safety properties involved. We highlight in particular the automated generation of invariant regions which turns out to be crucial in performing such verification. We use the hybrid system theorem prover KeymaeraX to formally check the parts of the proof that can be automatized in the current state of the tool.
    @article{Martin2017,
      author = {Martin, Benjamin and Ghorbal, Khalil and Goubault, Eric and Putot, Sylvie},
      title = {Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System},
      journal = {Electronic Proceedings in Theoretical Computer Science},
      year = {2017},
      volume = {257},
      pages = {91--104},
      month = sep,
      booktitle = {Proceedings First Workshop on Formal Verification of Autonomous Vehicles, FVAV@iFM 2017, Turin, Italy, 19th September 2017.},
      doi = {10.4204/eptcs.257.9},
      editor = {Bulwahn, Lukas and Kamali, Maryam and Linker, Sven},
      file = {:papers/stationkeeping.pdf:PDF},
      publisher = {Open Publishing Association},
      series = {{EPTCS}},
      timestamp = {Mon, 16 Oct 2017 16:32:11 +0200},
      url = {https://doi.org/10.4204/EPTCS.257.9}
    }
    
  4. Ghorbal K, Jeannin J-B, Zawadzki E, and others (2014) Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges. Journal of Aerospace Information Systems 11:702–713. doi: 10.2514/1.i010178
    Complex software systems are becoming increasingly prevalent in aerospace applications, in particular to accomplish critical tasks. Ensuring the safety of these systems is crucial, while they can have subtly different behavior under slight variations in op- erating conditions. In this paper we advocate the use of formal verification techniques and in particular theorem proving for hybrid software-intensive systems as a well- founded complementary approach to the classical aerospace verification and validation techniques such as testing or simulation. As an illustration of these techniques, we study a novel lateral mid-air collision avoidance maneuver in an ideal setting, without accounting for the uncertainties of the physical reality. We then detail the challenges that naturally arise when applying such technology to industrial-scale applications and our proposals on how to address these issues.
    @article{Ghorbal2014,
      author = {Ghorbal, Khalil and Jeannin, Jean-Baptiste and Zawadzki, Erik and Platzer, Andr{\'{e}} and Gordon, Geoffrey J. and Capell, Peter},
      title = {Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges},
      journal = {Journal of Aerospace Information Systems},
      year = {2014},
      volume = {11},
      number = {10},
      pages = {702--713},
      month = oct,
      doi = {10.2514/1.i010178},
      file = {:papers/jais2014.pdf:PDF},
      publisher = {American Institute of Aeronautics and Astronautics ({AIAA})},
      timestamp = {Tue, 06 Jun 2017 01:00:00 +0200},
      url = {https://doi.org/10.2514/1.I010178}
    }
    
  5. Mitsch S, Ghorbal K, Vogelbacher D, Platzer A (2017) Formal verification of obstacle avoidance and navigation of ground robots. The International Journal of Robotics Research 36:1312–1340. doi: 10.1177/0278364917733549
    This article answers fundamental safety questions for ground robot navigation: Under which circumstances does which control decision make a ground robot safely avoid obstacles? Unsurprisingly, the answer depends on the exact formulation of the safety objective as well as the physical capabilities and limitations of the robot and the obstacles. Because uncertainties about the exact future behavior of a robot’s environment make this a challenging problem, we formally verify corresponding controllers and provide rigorous safety proofs justifying why they can never collide with the obstacle in the respective physical model. To account for ground robots in which different physical phenomena are important, we analyze a series of increasingly strong properties of controllers for increasingly rich dynamics and identify the impact that the additional model parameters have on the required safety margins. We analyze and formally verify: (i) static safety, which ensures that no collisions can happen with stationary obstacles, (ii) passive safety, which ensures that no collisions can happen with stationary or moving obstacles while the robot moves, (iii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well, and (iv) passive orientation safety, which allows for imperfect sensor coverage of the robot, i.e., the robot is aware that not everything in its environment will be visible. We formally prove that safety can be guaranteed despite sensor uncertainty and actuator perturbation. We complement these provably correct safety properties with liveness properties: we prove that provably safe motion is flexible enough to let the robot navigate waypoints and pass intersections. In order to account for the mixed influence of discrete control decisions and the continuous physical motion of the ground robot, we develop corresponding hybrid system models and use differential dynamic logic theorem proving techniques to formally verify their correctness. Since these models identify a broad range of conditions under which control decisions are provably safe, our results apply to any control algorithm for ground robots with the same dynamics. As a demonstration, we, thus, also synthesize provably correct runtime monitor conditions that check the compliance of any control algorithm with the verified control decisions.
    @article{Mitsch2017,
      author = {Mitsch, Stefan and Ghorbal, Khalil and Vogelbacher, David and Platzer, Andr{\'{e}}},
      title = {Formal verification of obstacle avoidance and navigation of ground robots},
      journal = {The International Journal of Robotics Research},
      year = {2017},
      volume = {36},
      number = {12},
      pages = {1312--1340},
      month = oct,
      doi = {10.1177/0278364917733549},
      file = {:papers/morerobix.pdf:PDF},
      publisher = {{SAGE} Publications},
      timestamp = {Wed, 22 Nov 2017 17:24:54 +0100},
      url = {https://doi.org/10.1177/0278364917733549}
    }
    
  6. Sogokon A, Ghorbal K, Johnson TT (2017) Operational Models for Piecewise-Smooth Systems. ACM Transactions on Embedded Computing Systems 16:1–19. doi: 10.1145/3126506
    This paper studies ways of constructing meaningful operational models of piecewise-smooth systems (PWS). The systems we consider are described by polynomial vector fields defined on non-overlapping semi-algebraic sets, which form a partition of the state space. Our approach is to give meaning to motion in systems of this type by automatically synthesizing operational models in the form of hybrid automata (HA). Despite appearances, it is in practice often difficult to arrive at satisfactory HA models of PWS. The different ways of building operational models that we explore in our approach can be thought of as defining different semantics for the underlying PWS. These differences have a number of interesting nuances related to phenomena such as chattering, non-determinism, so-called mythical modes and sliding behaviour.
    @article{Sogokon2017,
      author = {Sogokon, Andrew and Ghorbal, Khalil and Johnson, Taylor T.},
      title = {Operational Models for Piecewise-Smooth Systems},
      journal = {{ACM} Transactions on Embedded Computing Systems},
      year = {2017},
      volume = {16},
      number = {5s},
      pages = {1--19},
      month = oct,
      issn = {1539-9087},
      acmid = {3126506},
      address = {New York, NY, USA},
      articleno = {185},
      doi = {10.1145/3126506},
      file = {:papers/op-semantics_emsoft17.pdf:PDF},
      issue_date = {October 2017},
      keywords = {Piecewise-smooth systems, discontinuous differential equations, hybrid automata, operational models},
      numpages = {19},
      publisher = {Association for Computing Machinery ({ACM})},
      url = {http://doi.acm.org/10.1145/3126506}
    }
    

Conferences

  1. Benveniste A, Caillaud B, Elmqvist H, and others (2017) Structural Analysis of Multi-Mode DAE Systems. In: Frehse G, Mitra S (eds) Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18-20, 2017. ACM Press, pp 253–263
    Differential Algebraic Equation (DAE) systems constitute the mathematical model supporting physical modeling languages such as Modelica, VHDL-AMS, or Simscape. Unlike ODEs, they exhibit subtle issues because of their implicit latent equations and related differentiation index. Multi-mode DAE (mDAE) systems are much harder to deal with, not only because of their mode-dependent dynamics, but essentially because of the events and resets occurring at mode transitions. Unfortunately, the large literature devoted to the numerical analysis of DAEs does not cover the multi-mode case. It typically says nothing about mode changes. This lack of foundations cause numerous difficulties to the existing modeling tools. Some models are well handled, others are not, with no clear boundary between the two classes. In this paper we develop a comprehensive mathematical approach to the structural analysis of mDAE systems which properly extends the usual analysis of DAE systems. We define a constructive semantics based on nonstandard analysis and show how to produce execution schemes in a systematic way.
    @inproceedings{Benveniste2017,
      author = {Benveniste, Albert and Caillaud, Benoit and Elmqvist, Hilding and Ghorbal, Khalil and Otter, Martin and Pouzet, Marc},
      title = {Structural Analysis of Multi-Mode {DAE} Systems},
      booktitle = {Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, {HSCC} 2017, Pittsburgh, PA, USA, April 18-20, 2017},
      year = {2017},
      editor = {Frehse, Goran and Mitra, Sayan},
      pages = {253--263},
      publisher = {{ACM} Press},
      doi = {10.1145/3049797.3049806},
      file = {:papers/hscc2017.pdf:PDF},
      timestamp = {Thu, 20 Apr 2017 15:40:48 +0200},
      url = {http://doi.acm.org/10.1145/3049797.3049806}
    }
    
  2. Sogokon A, Ghorbal K, Johnson TT (2016) Non-linear Continuous Systems for Safety Verification. In: Frehse G, Althoff M (eds) ARCH@CPSWeek 2016, 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Vienna, Austria. EasyChair, pp 42–51
    Safety verification of hybrid dynamical systems relies crucially on the ability to reason about reachable sets of continuous systems whose evolution is governed by a system of ordinary differential equations (ODEs). Verification tools are often restricted to handling a particular class of continuous systems, such as e.g. differential equations with constant right-hand sides, or systems of affine ODEs. More recently, verification tools capable of working with non-linear differential equations have been developed. The behavior of non-linear systems is known to be in general extremely difficult to analyze because solutions are rarely available in closed-form. In order to assess the practical utility of the various verification tools working with non-linear ODEs it is very useful to maintain a set of verification problems. Similar efforts have been successful in other communities, such as automated theorem proving, SAT solving and numerical analysis, and have accelerated improvements in the tools and their underlying algorithms. We present a set of 65 safety verification problems featuring non-linear polynomial ODEs and for which we have proofs of safety. We discuss the various issues associated with benchmarking the currently available verification tools using these problems.
    @inproceedings{Sogokon2016,
      author = {Sogokon, Andrew and Ghorbal, Khalil and Johnson, Taylor T.},
      title = {Non-linear Continuous Systems for Safety Verification},
      booktitle = {ARCH@CPSWeek 2016, 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Vienna, Austria},
      year = {2016},
      editor = {Frehse, Goran and Althoff, Matthias},
      volume = {43},
      series = {EPiC Series in Computing},
      pages = {42--51},
      publisher = {EasyChair},
      file = {:papers/arch2016.pdf:PDF},
      timestamp = {Tue, 25 Jul 2017 01:00:00 +0200},
      url = {http://www.easychair.org/publications/paper/334334}
    }
    
  3. Sogokon A, Ghorbal K, Johnson TT (2016) Decoupling Abstractions of Non-linear Ordinary Differential Equations. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds) FM 2016: Formal Methods. Springer International Publishing, pp 628–644
    We investigate decoupling abstractions, by which we seek to simulate (i.e. abstract) a given system of ordinary differential equations (ODEs) by another system that features completely independent (i.e. uncoupled) subsystems, which can be considered as separate systems in their own right. Beyond a purely mathematical interest as a tool for the qualitative analysis of ODEs, decoupling can be applied to verification problems arising in the fields of control and hybrid systems. Existing verification technology often scales poorly with dimension. Thus, reducing a verification problem to a number of independent verification problems for systems of smaller dimension may enable one to prove properties that are otherwise seen as too difficult. We show an interesting correspondence between Darboux polynomials and decoupling simulating abstractions of systems of polynomial ODEs and give a constructive procedure for automatically computing the latter.
    @inproceedings{Sogokon2016a,
      author = {Sogokon, Andrew and Ghorbal, Khalil and Johnson, Taylor T.},
      title = {Decoupling Abstractions of Non-linear Ordinary Differential Equations},
      booktitle = {{FM} 2016: Formal Methods},
      year = {2016},
      editor = {Fitzgerald, John S. and Heitmeyer, Constance L. and Gnesi, Stefania and Philippou, Anna},
      volume = {9995},
      series = {Lecture Notes in Computer Science},
      pages = {628--644},
      publisher = {Springer International Publishing},
      doi = {10.1007/978-3-319-48989-6_38},
      file = {:papers/fm2016.pdf:PDF},
      timestamp = {Mon, 22 May 2017 17:11:19 +0200},
      url = {https://doi.org/10.1007/978-3-319-48989-6_38}
    }
    
  4. Sogokon A, Ghorbal K, Jackson PB, Platzer A (2016) A Method for Invariant Generation for Polynomial Continuous Systems. In: Jobstmann B, Leino KRM (eds) Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. Springer, pp 268–288
    The paper presents a theoretical and experimental comparison of sound proof rules for proving invariance of algebraic sets, that is, sets satisfying polynomial equalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the trade-off between proof rule generality and practical performance and evaluate our theoretical observations on a set of heterogeneous benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting.
    @inproceedings{Sogokon2016b,
      author = {Sogokon, Andrew and Ghorbal, Khalil and Jackson, Paul B. and Platzer, Andr{\'{e}}},
      title = {A Method for Invariant Generation for Polynomial Continuous Systems},
      booktitle = {Verification, Model Checking, and Abstract Interpretation - 17th International Conference, {VMCAI} 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings},
      year = {2016},
      editor = {Jobstmann, Barbara and Leino, K. Rustan M.},
      volume = {9583},
      series = {Lecture Notes in Computer Science},
      pages = {268--288},
      publisher = {Springer},
      doi = {10.1007/978-3-662-49122-5_13},
      file = {:papers/vmcai2016.pdf:PDF},
      timestamp = {Mon, 05 Jun 2017 01:00:00 +0200},
      url = {https://doi.org/10.1007/978-3-662-49122-5_13}
    }
    
  5. Jeannin J-B, Ghorbal K, Kouskoulas Y, and others (2015) Formal verification of ACAS X, an industrial airborne collision avoidance system. In: Girault A, Guan N (eds) 2015 International Conference on Embedded Software, EMSOFT 2015, Amsterdam, Netherlands, October 4-9, 2015. IEEE, pp 127–136
    Formal verification of industrial systems is very challenging, due to reasons ranging from scalability issues to communication difficulties with engineering-focused teams. More importantly, industrial systems are rarely designed for verification, but rather for opera- tional needs. In this paper we present an overview of our experience using hybrid systems theorem proving to formally verify ACAS X, an airborne collision avoidance system for airliners scheduled to be operational around 2020. The methods and proof techniques presented here are an overview of the work already presented in an earlier work by the authors, while the evaluation of ACAS X has been significantly expanded and updated to the most recent version of the system, run 13. The effort presented in this paper is an integral part of the ACAS X development and was performed in tight collaboration with the ACAS X development team.
    @inproceedings{Jeannin2015,
      author = {Jeannin, Jean{-}Baptiste and Ghorbal, Khalil and Kouskoulas, Yanni and Gardner, Ryan and Schmidt, Aurora and Zawadzki, Erik and Platzer, Andr{\'{e}}},
      title = {Formal verification of {ACAS} X, an industrial airborne collision avoidance system},
      booktitle = {2015 International Conference on Embedded Software, {EMSOFT} 2015, Amsterdam, Netherlands, October 4-9, 2015},
      year = {2015},
      editor = {Girault, Alain and Guan, Nan},
      pages = {127--136},
      month = oct,
      publisher = {{IEEE}},
      doi = {10.1109/emsoft.2015.7318268},
      file = {:papers/acasx-emsoft15.pdf:PDF},
      timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
      url = {https://doi.org/10.1109/EMSOFT.2015.7318268}
    }
    
  6. Jeannin J-B, Ghorbal K, Kouskoulas Y, and others (2015) A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System. In: Baier C, Tinelli C (eds) Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Springer, pp 21–36
    The Next-Generation Airborne Collision Avoidance System (ACASX) is intended to be installed on all large aircraft to give advice to pilots and prevent mid-air collisions with other aircraft. It is currently being developed by the Federal Aviation Administration (FAA). In this paper we determine the geometric configurations under which the advice given by ACAS X is safe under a precise set of assumptions and formally verify these configurations using hybrid systems theorem proving techniques. We conduct an initial examination of the current version of the real ACAS X system and discuss some cases where our safety theorem conflicts with the actual advisory given by that version, demonstrating how formal, hybrid approaches are helping ensure the safety of ACAS X. Our approach is general and could also be used to identify unsafe advice issued by other collision avoidance systems or confirm their safety.
    @inproceedings{Jeannin2015a,
      author = {Jeannin, Jean{-}Baptiste and Ghorbal, Khalil and Kouskoulas, Yanni and Gardner, Ryan and Schmidt, Aurora and Zawadzki, Erik and Platzer, Andr{\'{e}}},
      title = {A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System},
      booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, {TACAS} 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2015, London, UK, April 11-18, 2015. Proceedings},
      year = {2015},
      editor = {Baier, Christel and Tinelli, Cesare},
      volume = {9035},
      series = {Lecture Notes in Computer Science},
      pages = {21--36},
      publisher = {Springer},
      doi = {10.1007/978-3-662-46681-0_2},
      file = {:papers/tacas2015.pdf:PDF},
      timestamp = {Thu, 15 Jun 2017 21:37:10 +0200},
      url = {https://doi.org/10.1007/978-3-662-46681-0_2}
    }
    
  7. Ghorbal K, Sogokon A, Platzer A (2015) A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets. In: D’Souza D, Lal A, Larsen KG (eds) Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings. Springer, pp 431–448
    This paper presents a theoretical and experimental comparison of sound proof rules for proving invariance of algebraic sets, that is, sets satisfying polynomial equalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the trade-off between proof rule generality and practical performance and evaluate our theoretical observations on a set of heterogeneous benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting.
    @inproceedings{Ghorbal2015,
      author = {Ghorbal, Khalil and Sogokon, Andrew and Platzer, Andr{\'{e}}},
      title = {A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets},
      booktitle = {Verification, Model Checking, and Abstract Interpretation - 16th International Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings},
      year = {2015},
      editor = {D'Souza, Deepak and Lal, Akash and Larsen, Kim Guldstrand},
      volume = {8931},
      series = {Lecture Notes in Computer Science},
      pages = {431--448},
      publisher = {Springer},
      doi = {10.1007/978-3-662-46081-8_24},
      file = {:papers/vmcai2015.pdf:PDF},
      timestamp = {Wed, 24 May 2017 08:30:31 +0200},
      url = {https://doi.org/10.1007/978-3-662-46081-8_24}
    }
    
  8. Ghorbal K, Sogokon A, Platzer A (2014) Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations. In: Müller-Olm M, Seidl H (eds) Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings. Springer, pp 151–167
    In this paper we seek to provide greater automation for formal deductive verification tools working with continuous and hybrid dynamical systems. We present an efficient procedure to check invariance of conjunctions of polynomial equalities under the flow of polynomial ordinary differential equations. The procedure is based on a necessary and sufficient condition that characterizes invariant conjunctions of polynomial equalities. We contrast this approach to an alternative one which combines fast and sufficient (but not necessary) conditions using differential cuts for soundly restricting the system evolution domain.
    @inproceedings{Ghorbal2014a,
      author = {Ghorbal, Khalil and Sogokon, Andrew and Platzer, Andr{\'{e}}},
      title = {Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations},
      booktitle = {Static Analysis - 21st International Symposium, {SAS} 2014, Munich, Germany, September 11-13, 2014. Proceedings},
      year = {2014},
      editor = {M{\"{u}}ller{-}Olm, Markus and Seidl, Helmut},
      volume = {8723},
      series = {Lecture Notes in Computer Science},
      pages = {151--167},
      publisher = {Springer},
      doi = {10.1007/978-3-319-10936-7_10},
      file = {:papers/sas2014.pdf:PDF},
      timestamp = {Wed, 24 May 2017 08:27:53 +0200},
      url = {https://doi.org/10.1007/978-3-319-10936-7_10}
    }
    
  9. Ghorbal K, Platzer A (2014) Characterizing Algebraic Invariants by Differential Radical Invariants. In: Ábrahám E, Havelund K (eds) Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings. Springer, pp 279–294
    We prove that any invariant algebraic set of a given polynomial vector field can be algebraically represented by one polynomial and a finite set of its successive Lie derivatives. This so-called differential radical characterization relies on a sound abstraction of the reachable set of solutions by the smallest variety that contains it. The characterization leads to a differential radical invariant proof rule that is sound and complete, which implies that invariance of algebraic equations over real-closed fields is decidable. Furthermore, the problem of generating invariant varieties is shown to be as hard as minimizing the rank of a symbolic matrix, and is therefore NP-hard. We investigate symbolic linear algebra tools based on Gaussian elimination to efficiently automate the generation. The approach can, e.g., generate nontrivial algebraic invariant equations capturing the airplane behavior during take-off or landing in longitudinal motion.
    
    @inproceedings{Ghorbal2014b,
      author = {Ghorbal, Khalil and Platzer, Andr{\'{e}}},
      title = {Characterizing Algebraic Invariants by Differential Radical Invariants},
      booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, {TACAS} 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2014, Grenoble, France, April 5-13, 2014. Proceedings},
      year = {2014},
      editor = {{\'{A}}brah{\'{a}}m, Erika and Havelund, Klaus},
      volume = {8413},
      series = {Lecture Notes in Computer Science},
      pages = {279--294},
      publisher = {Springer},
      doi = {10.1007/978-3-642-54862-8_19},
      file = {:papers/tacas2014.pdf:PDF},
      timestamp = {Mon, 05 Jun 2017 12:40:03 +0200},
      url = {https://doi.org/10.1007/978-3-642-54862-8_19}
    }
    
  10. Mitsch S, Ghorbal K, Platzer A (2013) On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles. In: Newman P, Fox D, Hsu D (eds) Robotics: Science and Systems IX, Technische Universität Berlin, Berlin, Germany, June 24 - June 28, 2013.
    Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and in close proximity with humans. Thus, safety of motion and obstacle avoidance are vital safety features of such robots. We formally study two safety properties of avoiding both stationary and moving obstacles: (i) passive safety, which ensures that no collisions can happen while the robot moves, and (ii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well. We use hybrid system models and theorem proving techniques that describe and formally verify the robot’s discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite location and actuator uncertainty.
    @inproceedings{Mitsch2013,
      author = {Mitsch, Stefan and Ghorbal, Khalil and Platzer, Andr{\'{e}}},
      title = {On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles},
      booktitle = {Robotics: Science and Systems IX, Technische Universit{\"{a}}t Berlin, Berlin, Germany, June 24 - June 28, 2013},
      year = {2013},
      editor = {Newman, Paul and Fox, Dieter and Hsu, David},
      file = {:papers/rss2013.pdf:PDF},
      timestamp = {Tue, 09 Feb 2016 15:15:28 +0100},
      url = {http://www.roboticsproceedings.org/rss09/p14.html}
    }
    
  11. Ghorbal K, Duggirala PS, Kahlon V, and others (2012) Efficient Probabilistic Model Checking of Systems with Ranged Probabilities. In: Finkel A, Leroux J, Potapov I (eds) Reachability Problems - 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings. Springer, pp 107–120
    We introduce a new technique to model check reachability properties on Interval Discrete-Time Markov Chains (IDTMC). We compute a sound over- approximation of the probabilities of satisfying a given property where the accuracy is characterized in terms of error bounds. We leverage affine arithmetic to propagate the first-order error terms. Higher-order error terms are bounded using interval arithmetic.
    @inproceedings{Ghorbal2012,
      author = {Ghorbal, Khalil and Duggirala, Parasara Sridhar and Kahlon, Vineet and Ivancic, Franjo and Gupta, Aarti},
      title = {Efficient Probabilistic Model Checking of Systems with Ranged Probabilities},
      booktitle = {Reachability Problems - 6th International Workshop, {RP} 2012, Bordeaux, France, September 17-19, 2012. Proceedings},
      year = {2012},
      editor = {Finkel, Alain and Leroux, J{\'{e}}r{\^{o}}me and Potapov, Igor},
      volume = {7550},
      series = {Lecture Notes in Computer Science},
      pages = {107--120},
      publisher = {Springer},
      doi = {10.1007/978-3-642-33512-9_10},
      file = {:papers/rp12.pdf:PDF},
      timestamp = {Fri, 26 May 2017 01:00:00 +0200},
      url = {https://doi.org/10.1007/978-3-642-33512-9_10}
    }
    
  12. Ghorbal K, Ivancic F, Balakrishnan G, and others (2012) Donut Domains: Efficient Non-convex Domains for Abstract Interpretation. In: Kuncak V, Rybalchenko A (eds) Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings. Springer, pp 235–250
    Program analysis using abstract interpretation has been successfully applied in practice to find runtime bugs or prove software correct. Most abstract domains that are used widely rely on convexity for their scalability. However, the ability to express non-convex properties is sometimes required in order to achieve a precise analysis of some numerical properties. This work combines already known abstract domains in a novel way in order to design new abstract domains that tackle some non-convex invariants. The abstract objects of interest are encoded as a pair of two convex abstract objects: the first abstract object defines an over-approximation of the possible reached values, as is done customarily. The second abstract object under-approximates the set of impossible values within the state-space of the first abstract object. Therefore, the geometrical concretization of our objects is defined by a convex set minus another convex set (or hole). We thus call these domains donut domains.
    @inproceedings{Ghorbal2012a,
      author = {Ghorbal, Khalil and Ivancic, Franjo and Balakrishnan, Gogul and Maeda, Naoto and Gupta, Aarti},
      title = {Donut Domains: Efficient Non-convex Domains for Abstract Interpretation},
      booktitle = {Verification, Model Checking, and Abstract Interpretation - 13th International Conference, {VMCAI} 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings},
      year = {2012},
      editor = {Kuncak, Viktor and Rybalchenko, Andrey},
      volume = {7148},
      series = {Lecture Notes in Computer Science},
      pages = {235--250},
      publisher = {Springer},
      doi = {10.1007/978-3-642-27940-9_16},
      file = {:papers/vmcai2012.pdf:PDF},
      timestamp = {Wed, 24 May 2017 08:30:31 +0200},
      url = {https://doi.org/10.1007/978-3-642-27940-9_16}
    }
    
  13. Ghorbal K, Goubault E, Putot S (2010) A Logical Product Approach to Zonotope Intersection. In: Touili T, Cook B, Jackson PB (eds) Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. Springer, pp 212–226
    We define and study a new abstract domain which is a fine-grained combination of zonotopes with (sub-)polyhedric domains such as the interval, octagon, linear template or polyhedron domains. While abstract transfer functions are still rather inexpensive and accurate even for interpreting non-linear computations, we are able to also interpret tests (i.e. intersections) efficiently. This fixes a known drawback of zonotopic methods, as used for reachability analysis for hybrid systems as well as for invariant generation in abstract interpretation: intersection of zonotopes are not always zonotopes, and there is not even a best zonotopic over-approximation of the intersection. We describe some examples and an implementation of our method in the APRON library, and discuss some further interesting combinations of zonotopes with non-linear or non-convex domains such as quadratic templates and maxplus polyhedra.
    
    @inproceedings{Ghorbal2010,
      author = {Ghorbal, Khalil and Goubault, Eric and Putot, Sylvie},
      title = {A Logical Product Approach to Zonotope Intersection},
      booktitle = {Computer Aided Verification, 22nd International Conference, {CAV} 2010, Edinburgh, UK, July 15-19, 2010. Proceedings},
      year = {2010},
      editor = {Touili, Tayssir and Cook, Byron and Jackson, Paul B.},
      volume = {6174},
      series = {Lecture Notes in Computer Science},
      pages = {212--226},
      publisher = {Springer},
      doi = {10.1007/978-3-642-14295-6_22},
      file = {:papers/cav2010.pdf:PDF},
      timestamp = {Thu, 25 May 2017 01:00:00 +0200},
      url = {https://doi.org/10.1007/978-3-642-14295-6_22}
    }
    
  14. Ghorbal K, Goubault E, Putot S (2009) The Zonotope Abstract Domain Taylor1+. In: Bouajjani A, Maler O (eds) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Springer, pp 627–633
    Static analysis by abstract interpretation aims at automatically inferring properties on the behaviour of programs. We focus here on a specific kind of numerical invariants: the set of values taken by numerical variables, with a real numbers semantics, at each control point of a program. We present an implementation called Taylor1+, interfaced with the APRON library, of an abstract domain using affine forms. 
    @inproceedings{Ghorbal2009,
      author = {Ghorbal, Khalil and Goubault, Eric and Putot, Sylvie},
      title = {The Zonotope Abstract Domain Taylor1+},
      booktitle = {Computer Aided Verification, 21st International Conference, {CAV} 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},
      year = {2009},
      editor = {Bouajjani, Ahmed and Maler, Oded},
      volume = {5643},
      series = {Lecture Notes in Computer Science},
      pages = {627--633},
      publisher = {Springer},
      doi = {10.1007/978-3-642-02658-4_47},
      file = {:papers/cav2009.pdf:PDF},
      timestamp = {Thu, 25 May 2017 01:00:00 +0200},
      url = {https://doi.org/10.1007/978-3-642-02658-4_47}
    }
    

Thesis

  1. Ghorbal K (2011) Static Analysis of Numerical Programs: Constrained Affine Sets Abstract Domain. (Analyse Statique de Programmes Numériques: Ensembles Affines Contraints). PhD thesis, École Polytechnique, Palaiseau, France
    We aim at proving automatically the correctness of numerical behavior of a program by inferring invariants on numerical variables. More precisely, we over-approximate in a sound manner the set of reached values. We use Abstract Interpretation-based Static Analysis as a generic framework to define and approximate the semantics of a program in a unified manner. The semantics that describe the real behavior of the program (concrete semantics) is in general undecidable. Abstract interpretation offers a way to abstract this concrete semantics to obtain a decidable semantics involving machine-expressible objects. We introduce a new affine forms-based abstract domain, called constrained affine sets, which extends and generalizes an already existing abstract domain introduced by Eric Goubault and Sylvie Putot. The expressiveness of such new domain is enhanced thanks to its ability to encode and propagate linear constraints among variables. We have implemented our new domain to experiment the precision and the efficiency of our approach and compare our results to the already existing abstract domains. The theoretical work as well as the implementation and the experiments have been the subject of two publications at the Computer-Aided Verification (CAV) conference.  
    @phdthesis{Ghorbal2011,
      author = {Ghorbal, Khalil},
      title = {Static Analysis of Numerical Programs: Constrained Affine Sets Abstract Domain. (Analyse Statique de Programmes Num{\'{e}}riques: Ensembles Affines Contraints)},
      school = {{\'{E}}cole Polytechnique, Palaiseau, France},
      year = {2011},
      file = {:papers/thesis-KG.pdf:PDF},
      timestamp = {Mon, 11 Jul 2016 01:00:00 +0200},
      url = {https://tel.archives-ouvertes.fr/pastel-00643442}
    }