Mots-clés

Nombre de documents

22

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.


Article dans une revue5 documents

  • Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, André Platzer. Formal verification of obstacle avoidance and navigation of ground robots. International Journal of Robotics Research, SAGE Publications, 2017, 36 (12), pp.1312--1340. 〈10.1177/0278364917733549〉. 〈hal-01658197〉
  • 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〉
  • 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〉

Communication dans un congrès15 documents

  • 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. 2017, 〈http://hscc2017.ece.illinois.edu〉. 〈10.1145/3049797.3049806〉. 〈hal-01521918〉
  • Benjamin Martin, Khalil Ghorbal, Eric Goubault, Sylvie Putot. Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System. Lukas Bulwahn; Maryam Kamali; Sven Linker. FVAV 2017 - 1st Formal Verification of Autonomous Vehicles Workshop, Sep 2017, Turin, Italy. EPTCS, 257, pp.91--104, 2017, FVAV@iFM 2017. 〈https://sites.google.com/site/fvav2017/〉. 〈10.4204/EPTCS.257.9〉. 〈hal-01657848〉
  • Andrew Sogokon, Khalil Ghorbal, Taylor T. Johnson. Non-linear Continuous Systems for Safety Verification (Benchmark Proposal). Goran Frehse and Matthias Althoff. ARCH@CPSWeek 2016 - 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Apr 2016, Vienna, Austria. EasyChair, 43, pp.42-51, 2016, EPiC Series in Computing. 〈https://cps-vo.org/group/ARCH〉. 〈hal-01660900〉
  • Andrew Sogokon, Khalil Ghorbal, Paul Jackson, André Platzer. A Method for Invariant Generation for Polynomial Continuous Systems. Barbara Jobstmann; K. Rustan M. Leino. VMCAI 2016 - 17th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2016, St. Petersburg, Florida, United States. Springer, Lecture Notes in Computer Science, 9583, pp.268-288, 2016, Verification, Model Checking, and Abstract Interpretation. 〈http://link.springer.com/chapter/10.1007%2F978-3-662-49122-5_13〉. 〈10.1007/978-3-662-49122-5_13〉. 〈hal-01374902〉
  • 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. Springer, FM 2016: Formal Methods, 9995, pp.628-644, Lecture Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007/978-3-319-48989-6_38〉. 〈10.1007/978-3-319-48989-6_38〉. 〈hal-01374899v2〉
  • Khalil Ghorbal, Andrew Sogokon, André Platzer. A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets. Deepak D'Souza and Akash Lal and Kim Guldstrand Larsen. Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, 2015, Mumbai, India. Springer, 8931, pp.431--448, 2015, Lecture Notes in Computer Science. 〈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. Christel Baier and Cesare Tinelli. 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. Springer, 9035, pp.21--36, 2015, Lecture Notes in Computer Science. 〈10.1007/978-3-662-46681-0_2〉. 〈hal-01660903〉
  • Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, et al.. Formal verification of ACAS X, an industrial airborne collision avoidance system. Alain Girault and Nan Guan. 2015 International Conference on Embedded Software, EMSOFT 2015, Amsterdam, Netherlands, October 4-9, 2015, 2015, Amsterdam, Netherlands. IEEE, 2015 International Conference on Embedded Software, EMSOFT 2015, Amsterdam, Netherlands, October 4-9, 2015, pp.127--136, 2015, 〈10.1109/EMSOFT.2015.7318268〉. 〈hal-01660902〉
  • Khalil Ghorbal, Andrew Sogokon, André Platzer. Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations. Markus Müller-Olm and Helmut Seidl. Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, 2014, Munich, Germany. Springer, 8723, pp.151--167, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-10936-7_10〉. 〈hal-01660906〉
  • Khalil Ghorbal, André Platzer. Characterizing Algebraic Invariants by Differential Radical Invariants. Erika Ábrahám and Klaus Havelund. 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. Springer, 8413, pp.279--294, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-642-54862-8_19〉. 〈hal-01660904〉
  • Stefan Mitsch, Khalil Ghorbal, André Platzer. On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles. Paul Newman and Dieter Fox and David Hsu. Robotics: Science and Systems IX, Technische Universität Berlin, Berlin, Germany, June 24 - June 28, 2013, 2013, Berlin, Germany. Robotics: Science and Systems IX, Technische Universität Berlin, Berlin, Germany, June 24 - June 28, 2013, 2013. 〈hal-01660907〉
  • Khalil Ghorbal, Parasara Sridhar Duggirala, Vineet Kahlon, Franjo Ivancic, Aarti Gupta. Efficient Probabilistic Model Checking of Systems with Ranged Probabilities. Alain Finkel; Jérôme Leroux; Igor Potapov. RP 2012 - Reachability Problems - 6th International Workshop, Sep 2012, Bordeaux, France. Springer, 7550, pp.107--120, 2012, Lecture Notes in Computer Science. 〈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. Viktor Kuncak; Andrey Rybalchenko. VMCAI 2012 - Verification, Model Checking, and Abstract Interpretation - 13th International Conference, Jan 2012, Philadelphia, United States. Springer, 7148, pp.235--250, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-27940-9_16〉. 〈hal-01660908〉
  • Khalil Ghorbal, Eric Goubault, Sylvie Putot. A Logical Product Approach to Zonotope Intersection. Tayssir Touili and Byron Cook and Paul B. Jackson. Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, 2010, Edinburgh, United Kingdom. Springer, 6174, pp.212--226, 2010, Lecture Notes in Computer Science. 〈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, May 2009, Istambul, Turkey. European Space Agency, 1, pp.1-7, 2009. 〈inria-00528590〉

Rapport1 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〉

Thèse1 document

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