Khalil Ghorbal's Homepage

Khalil Ghorbal

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

I am currently a Postdoc at NEC Labs, System Analysis and Verification Group, Princeton, New Jersey, USA.

Research

Interests

Static Analysis based Abstract Interpretation
Affine Forms (Zonotopic Abstract Domain)
Convex analysis and optimization
Formal and automated methods to prove the safety of software (both theory and practise)
Semantics

Academic Projects

ASOPT (Static analysis and optimization), ANR Project. (2009-2012)
PASO (Preuve, Analyse Statique, Optimisation), DIGITEO Project. (2009-2011)

Publications

(DBLP)

[2012] 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). Co-authored with F. Ivancic, G. Balakrishnan, N. Maeda and A. Gupta. [to appear]

[2010] A logical product approach to zonotope intersection. In Proc. of the 22th Int. Conf. on Computer Aided Verification (CAV 2010). Co-authored with E. Goubault and S. Putot. [pdf | bib]

[2009] The zonotope abstract domain Taylor1+. In Proc. of the 21th Int. Conf. on Computer Aided Verification (CAV 2009). Co-authored with E. Goubault and S. Putot. [pdf | bib]

[2009] Space software validation using abstract interpretation. In Proc. of the Int. Space System Engineering Conf., Data Systems in Aerospace (DASIA 2009). Co-authored with O. Bouissou, E. Conquet, P. Cousot, R. Cousot, J. Feret, E. Goubault, D. Lesens, L. Mauborgne, A. Miné, S. Putot, X. Rival, and M. Turin. [pdf | bib]

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

NEC Labs, Suite 200
4 Independance Way
Princeton, 08540, New Jersey
USA

Phone: +1 609 951 2779

Fax: +1 609 951 2483

Speak Out Tunisia