Khalil Ghorbal
[photo]

NSV-2014

The 7th edition of the NSV Workshop, will be collocated with the Vienna Summer of Logic (FLOC 2014), July 12th-24th, 2014, at the Vienna University of Technology (TU Vienna).

Research

Interests

Projects

Publications

(DBLP)

[2014] Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In Proc. of the Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). [Talk | pdf | TechReport | bib]
[2013] Mitsch, S., Ghorbal, K., Platzer, A.: On provably safe obstacle avoidance for autonomous robotic ground vehicles. In Proc. of the Int. Conf. on Robotics: Science and Systems (RSS 2013). [pdf | bib]
[2012] Ghorbal, K., Duggirala, P. S., Ivančić, F., Kahlon, V., Gupta, A.: Efficient probabilistic model checking of systems with ranged probabilities. In the 6th Int. Work. on Reachability Problems (RP 2012). [pdf | bib]
[2012] Ghorbal, K., Ivančić, F., Balakrishnan, G., Maeda, N., Gupta, A.: Donut domains: efficient non-convex domains for abstract interpretation. In Proc. of the 13th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI 2012). [pdf | bib]
[2010] Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to zonotope intersection. In Proc. of the 22th Int. Conf. on Computer Aided Verification (CAV 2010). [pdf | bib]
[2009] Ghorbal, K., Goubault, E., Putot, S.: The zonotope abstract domain Taylor1+. In Proc. of the 21th Int. Conf. on Computer Aided Verification (CAV 2009). [pdf | bib]
[2009] Bouissou, O., Conquet, E., Cousot, P., Cousot, R., Feret, J., Ghorbal, K., Goubault, E., Lesens, D., Mauborgne, L., Miné, A., Putot, S., Rival, X., and Turin, T.: Space software validation using abstract interpretation. In Proc. of the Int. Space System Engineering Conf., Data Systems in Aerospace (DASIA 2009). [pdf | bib]

Thesis

[2011] Static Analysis of Numerical Programs: Constrained Affine Sets Abstract Domain. [pdf | slides]

Teaching

[2009] Instructor (vacataire, chargé de TDs) at École Nationale Supérieur des Techniques Avancées, Paris, France. Course. IN104 - Prim and Kruskal algorithms to build a perfect maze: learning the basic concepts to develop a computer program (analysis, specification, implementation, testing, etc.). Undergraduate, L3.
[2009] Instructor (vacataire, chargé de TDs) at École Nationale de la Statistique et de l'Administration Économique, Malakoff, France. Course. C++ language - basic concepts of object oriented programming language. Graduate, M1.
[2008] Instructor (vacataire, chargé de TDs) at École Polytechnique, Palaiseau, France. Course. Modex Web - a step by step tutorial to build its own web site, visiting the basic web technologies: HTML, CSS, PHP and Javascript. Graduate, M1.
[2008] Instructor (vacataire, chargé de TDs) at École Polytechnique, Palaiseau, France. Course. Mineure Parallélisme - Parallel Random Access Machine, Java Threads, Remote Method Invocation. Graduate, M2.

Software

Taylor1+
A constrained zonotopic abstract domain based on first Taylor Series approximations for non linear operations.
(Interfaced with APRON Library).
Benchmarks (CAV 2010)
You can find here some of the programs (written in SIMPLE language) used to compare the different APRON abstract domains (Boxes, Octagons, Polyhedra and Taylor1+).
Benchmarks (Donut Domains)
You can find here some examples of programs (written in SIMPLE language) with safe division-by-zero tests but hard to prove with classical domains.

Contact

I am currently a Postdoc at Carnegie Mellon University, School of Computer Science, Logical Systems Lab.

I was previously at NEC Labs, System Analysis and Verification Group, Princeton, New Jersey, USA.

I was a Ph.D. student in computer science, under the direction of Éric Goubault and Sylvie Putot.

c/o
Carnegie Mellon
Computer Science Department
Gates-Hillman Center . GHC-9008
5000 Forbes Avenue
Pittsburgh, PA 15213
USA

Phone: +1 412 268 7663

Fax: +1 412 268 5576