Preprints

  1. Ghorbal K, Kozaily C (2022) On Covering Smooth Manifolds with Overlapping Simplicies: An inductive Characterization of Q-matrices 
    This paper is concerned with a covering problem of smooth manifolds of dimension n-1 using a specific arrangement, called Q-arrangement, of 2^n n-simplices which could be degenerate and are allowed to overlap (preventing therefore the immediate use of simplicial homology). We leverage the underlying inductive nature of the problem to give a (non-constructive) topological characterization. We show that for low dimensions such characterization reduces to studying the local geometry around the specific points serving to form the simplices, solving thereby the problem for n ≤3. The motivation of such work comes from a relatively old, yet unsolved, problem that originated in the optimization community: under which conditions on the n\times n matrix M, does the so called linear complementarity problem given by w - M z = q, w,z≥0, and w.z = 0, have a solution (w,z) for all vectors q∈\mathbbR^n. If the latter property holds, the matrix M is said to be a Q-matrix.
    @preprint{Ghorbal2022a,
  author = {Ghorbal, Khalil and Kozaily, Christelle},
  title = {On Covering Smooth Manifolds with Overlapping Simplicies: An inductive Characterization of Q-matrices},
  year = {2022},
  month = mar,
  archiveprefix = {arXiv},
  eprint = {2203.12333},
  keywords = {math.AT, math.OC, 55U10, 90C26},
  primaryclass = {math.AT},
  url = {https://arxiv.org/pdf/2203.12333v2.pdf}
}
  2. Thibault J, Ghorbal K (2020) Ordered Functional Decision Diagrams: A Functional Semantics For Binary Decision Diagrams 
    We introduce a novel framework, termed \lambdaDD, that revisits Binary Decision Diagrams from a purely functional point of view. The framework allows to classify the already existing variants, including the most recent ones like Chain-DD and ESRBDD, as implementations of a special class of ordered models. We enumerate, in a principled way, all the models of this class and isolate its most expressive model. This new model, termed \lambdaDD-O-NUCX, is suitable for both dense and sparse Boolean functions, and is moreover invariant by negation. The canonicity of \lambdaDD-O-NUCX is formally verified using the Coq proof assistant. We furthermore give bounds on the size of the different diagrams: the potential gain achieved by more expressive models can be at most linear in the number of variables n.
    @preprint{Thibault2020,
  author = {Thibault, Joan and Ghorbal, Khalil},
  title = {Ordered Functional Decision Diagrams: A Functional Semantics For Binary Decision Diagrams},
  year = {2020},
  month = mar,
  archiveprefix = {arXiv},
  eprint = {2003.09340},
  keywords = {cs.LO, cs.AI, D.3.1; E.1; G.2.2},
  primaryclass = {cs.LO},
  url = {https://arxiv.org/pdf/2003.09340v4.pdf}
}

Journal Articles

  1. Ghorbal K, Sogokon A (2022) Characterizing positively invariant sets: Inductive and topological methods. Journal of Symbolic Computation 113:1–28. https://doi.org/10.1016/j.jsc.2022.01.004 
    We present two characterizations of positive invariance of sets under the flow of systems of ordinary differential equations. The first characterization uses inward sets which intuitively collect those points from which the flow evolves within the set for a short period of time, whereas the second characterization uses the notion of exit sets, which intuitively collect those points from which the flow immediately leaves the set. Our proofs emphasize the use of the real induction principle as a generic and unifying proof technique that captures the essence of the formal reasoning justifying our results and provides cleaner alternative proofs of known results. The two characterizations presented in this article, while essentially equivalent, lead to two rather different decision procedures (termed respectively LZZ and ESE) for checking whether a given semi-algebraic set is positively invariant under the flow of a system of polynomial ordinary differential equations. The procedure LZZ improves upon the original work by Liu, Zhan and Zhao (Liu et al., 2011). The procedure ESE, introduced in this article, works by splitting the problem, in a principled way, into simpler sub-problems that are easier to check, and is shown to exhibit substantially better performance compared to LZZ on problems featuring semi-algebraic sets described by formulas with non-trivial Boolean structure.
    @article{Ghorbal2022,
  author = {Ghorbal, Khalil and Sogokon, Andrew},
  journal = {Journal of Symbolic Computation},
  title = {Characterizing positively invariant sets: Inductive and topological methods},
  year = {2022},
  month = nov,
  pages = {1--28},
  volume = {113},
  doi = {10.1016/j.jsc.2022.01.004},
  file = {:papers/jsc2022.pdf:PDF},
  publisher = {Elsevier {BV}}
}
  2. 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. https://doi.org/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}
}
  3. 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. https://doi.org/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}}},
  journal = {International Journal on Software Tools for Technology Transfer},
  title = {A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system},
  year = {2017},
  month = oct,
  number = {6},
  pages = {717--741},
  volume = {19},
  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}
}
  4. 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. https://doi.org/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}
}
  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. https://doi.org/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. https://doi.org/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}
}
  7. 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. https://doi.org/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}
}

Conferences

  1. Sogokon A, Ghorbal K, Tan YK, Platzer A (2018) Vector Barrier Certificates and Comparison Systems. In: Formal Methods. Springer International Publishing, pp 418–437 
    Vector Lyapunov functions are a multi-dimensional extension of the more familiar (scalar) Lyapunov functions, commonly used to prove stability properties in systems of non-linear ordinary differen- tial equations (ODEs). This paper explores an analogous vector extension for so-called barrier certificates used in safety verification. As with vector Lyapunov functions, the approach hinges on constructing appropriate comparison systems, i.e., related differential equation systems from which properties of the original system may be inferred. The paper presents an accessible development of the approach, demonstrates that most previous notions of barrier certificate are special cases of comparison systems, and discusses the potential applications of vector barrier certificates in safety verification and invariant synthesis.
    @inproceedings{Sogokon2018,
  author = {Sogokon, Andrew and Ghorbal, Khalil and Tan, Yong Kiam and Platzer, Andr{\'{e}}},
  title = {Vector Barrier Certificates and Comparison Systems},
  booktitle = {Formal Methods},
  year = {2018},
  pages = {418--437},
  publisher = {Springer International Publishing},
  doi = {10.1007/978-3-319-95582-7_25},
  file = {:papers/fm2018.pdf:PDF}
}
  2. 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}
}
  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. 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}
}
  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. 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}
}
  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}}},
  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},
  title = {Characterizing Algebraic Invariants by Differential Radical Invariants},
  year = {2014},
  editor = {{\'{A}}brah{\'{a}}m, Erika and Havelund, Klaus},
  pages = {279--294},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {8413},
  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. 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}
}
  11. 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}
}
  12. 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}
}
  13. 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}
}
  14. 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},
  booktitle = {Computer Aided Verification, 22nd International Conference, {CAV} 2010, Edinburgh, UK, July 15-19, 2010. Proceedings},
  title = {A Logical Product Approach to Zonotope Intersection},
  year = {2010},
  editor = {Touili, Tayssir and Cook, Byron and Jackson, Paul B.},
  pages = {212--226},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6174},
  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}
}
  15. 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},
  booktitle = {Computer Aided Verification, 21st International Conference, {CAV} 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},
  title = {The Zonotope Abstract Domain Taylor1+},
  year = {2009},
  editor = {Bouajjani, Ahmed and Maler, Oded},
  pages = {627--633},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5643},
  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},
  school = {{\'{E}}cole Polytechnique, Palaiseau, France},
  title = {Static Analysis of Numerical Programs: Constrained Affine Sets Abstract Domain. (Analyse Statique de Programmes Num{\'{e}}riques: Ensembles Affines Contraints)},
  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}
}