Keywords

Number of documents

23

Khalil Ghorbal


I am currently a researcher at INRIA (Rennes, France), in the Hycomes group. My research focuses on advancing and promoting the use of formal methods to design and analyze industrial-scale complex systems.


Journal articles5 documents

  • Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, et al.. A Formally Verified Hybrid System for Safe Advisories in the Next-Generation Airborne Collision Avoidance System. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017, 19 (6), pp.717-741. ⟨10.1007/s10009-016-0434-1⟩. ⟨hal-01232365⟩
  • Andrew Sogokon, Khalil Ghorbal, Taylor Johnson. Operational Models for Piecewise-Smooth Systems. ACM Transactions on Embedded Computing Systems (TECS), ACM, 2017, 16 (5s), pp.185:1--185:19. ⟨10.1145/3126506⟩. ⟨hal-01658196⟩
  • Khalil Ghorbal, Andrew Sogokon, André Platzer. A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Computer Languages, Systems and Structures, Elsevier, 2017, Special issue on the 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), 47 (1), pp.19-43. ⟨10.1016/j.cl.2015.11.003⟩. ⟨hal-01232288⟩
  • Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, André Platzer. Formal verification of obstacle avoidance and navigation of ground robots. The International Journal of Robotics Research, SAGE Publications, 2017, 36 (12), pp.1312--1340. ⟨10.1177/0278364917733549⟩. ⟨hal-01658197⟩
  • Khalil Ghorbal, Jean-Baptiste Jeannin, Erik Zawadzki, André Platzer, Geoffrey J. Gordon, et al.. Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges. J. Aerospace Inf. Sys., 2014, 11 (10), pp.702--713. ⟨10.2514/1.I010178⟩. ⟨hal-01660905⟩

Conference papers16 documents

  • Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer. Vector Barrier Certificates and Comparison Systems. FM 2018 - 22nd International Symposium on Formal Methods, Jul 2018, Oxford, United Kingdom. pp.418-437, ⟨10.1007/978-3-319-95582-7_25⟩. ⟨hal-01969800⟩
  • Benjamin Martin, Khalil Ghorbal, Eric Goubault, Sylvie Putot. Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System. FVAV 2017 - 1st Formal Verification of Autonomous Vehicles Workshop, Sep 2017, Turin, Italy. pp.91--104, ⟨10.4204/EPTCS.257.9⟩. ⟨hal-01657848⟩
  • Albert Benveniste, Benoît Caillaud, Hilding Elmqvist, Khalil Ghorbal, Martin Otter, et al.. Structural Analysis of Multi-Mode DAE Systems. Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017, Apr 2017, Pittsburgh, PA, United States. ⟨10.1145/3049797.3049806⟩. ⟨hal-01521918⟩
  • Andrew Sogokon, Khalil Ghorbal, Taylor Johnson. Decoupling Abstractions of Non-linear Ordinary Differential Equations. FM 2016 - 21st International Symposium of Formal Methods, Nov 2016, Limassol, Cyprus. pp.628-644, ⟨10.1007/978-3-319-48989-6_38⟩. ⟨hal-01374899v2⟩
  • Andrew Sogokon, Khalil Ghorbal, Paul Jackson, André Platzer. A Method for Invariant Generation for Polynomial Continuous Systems. VMCAI 2016 - 17th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2016, St. Petersburg, Florida, United States. pp.268-288, ⟨10.1007/978-3-662-49122-5_13⟩. ⟨hal-01374902⟩
  • Andrew Sogokon, Khalil Ghorbal, Taylor T. Johnson. Non-linear Continuous Systems for Safety Verification (Benchmark Proposal). ARCH@CPSWeek 2016 - 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Apr 2016, Vienna, Austria. pp.42-51. ⟨hal-01660900⟩
  • Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, et al.. Formal verification of ACAS X, an industrial airborne collision avoidance system. 2015 International Conference on Embedded Software, EMSOFT 2015, Amsterdam, Netherlands, October 4-9, 2015, 2015, Amsterdam, Netherlands. pp.127--136, ⟨10.1109/EMSOFT.2015.7318268⟩. ⟨hal-01660902⟩
  • Khalil Ghorbal, Andrew Sogokon, André Platzer. A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets. Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, 2015, Mumbai, India. pp.431--448, ⟨10.1007/978-3-662-46081-8_24⟩. ⟨hal-01660901⟩
  • Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, et al.. A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System. 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, 2015, London, United Kingdom. pp.21--36, ⟨10.1007/978-3-662-46681-0_2⟩. ⟨hal-01660903⟩
  • Khalil Ghorbal, André Platzer. Characterizing Algebraic Invariants by Differential Radical Invariants. 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, 2014, Grenoble, France. pp.279--294, ⟨10.1007/978-3-642-54862-8_19⟩. ⟨hal-01660904⟩
  • Khalil Ghorbal, Andrew Sogokon, André Platzer. Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations. Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, 2014, Munich, Germany. pp.151--167, ⟨10.1007/978-3-319-10936-7_10⟩. ⟨hal-01660906⟩
  • Stefan Mitsch, Khalil Ghorbal, André Platzer. On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles. Robotics: Science and Systems IX, Technische Universität Berlin, Berlin, Germany, June 24 - June 28, 2013, 2013, Berlin, Germany. ⟨hal-01660907⟩
  • Khalil Ghorbal, Parasara Sridhar Duggirala, Vineet Kahlon, Franjo Ivancic, Aarti Gupta. Efficient Probabilistic Model Checking of Systems with Ranged Probabilities. RP 2012 - Reachability Problems - 6th International Workshop, Sep 2012, Bordeaux, France. pp.107--120, ⟨10.1007/978-3-642-33512-9_10⟩. ⟨hal-01660909⟩
  • Khalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta. Donut Domains: Efficient Non-convex Domains for Abstract Interpretation. VMCAI 2012 - Verification, Model Checking, and Abstract Interpretation - 13th International Conference, Jan 2012, Philadelphia, United States. pp.235--250, ⟨10.1007/978-3-642-27940-9_16⟩. ⟨hal-01660908⟩
  • Khalil Ghorbal, Eric Goubault, Sylvie Putot. A Logical Product Approach to Zonotope Intersection. Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, 2010, Edinburgh, United Kingdom. pp.212--226, ⟨10.1007/978-3-642-14295-6_22⟩. ⟨hal-01660910⟩
  • Olivier Bouissou, Eric Conquet, Patrick Cousot, Radhia Cousot, Jérôme Feret, et al.. Space Software Validation using Abstract Interpretation. The International Space System Engineering Conference : Data Systems in Aerospace - DASIA 2009, EUROSPACE, May 2009, Istambul, Turkey. pp.1-7. ⟨inria-00528590⟩

Reports1 document

  • Albert Benveniste, Benoît Caillaud, Hilding Elmqvist, Khalil Ghorbal, Martin Otter, et al.. Structural Analysis of Multi-Mode DAE Systems. [Research Report] RR-8933, Inria. 2017, pp.1-23. ⟨hal-01343967v3⟩

Theses1 document

  • Khalil Ghorbal. Static Analysis of Numerical Programs: Constrained Affine Sets Abstract Domain. Symbolic Computation [cs.SC]. Ecole Polytechnique X, 2011. English. ⟨pastel-00643442⟩