Qui suis-je ?

Je m'appelle Ghiles Ziat et je suis enseignant-chercheur à l' (EPITA), au sein du LRE dans l'équipe Automates. Je m'intéresse aux méthodes formelles, et en particulier à l'analyse statique de programmes et à la programmation par contraintes.

Avant ça j'ai fais un premier post-doctorat à l'ISAE-SUPAERO, au DISC sous la supervision de Christophe Garion et Xavier Thirioux. Nous nous sommes intéressés à l'analyse de systèmes hybrides par une approche CP/IA. J'ai ensuite été post-doctorant à au laboratoire d'Informatique de l'Université de Paris (IRIF), au sein du groupe Preuves, Programmes et Systèmes, où je me suis interessé à l'analyse statique de tests.

J'ai fais ma thèse, dans l'équipe APR du LIP6. Mes encadrants étaient Antoine Miné et Charlotte Truchet. Mon sujet de recherche était l'étude des combinaisons entre l'interpretation abstraite et la programmation par contraintes. Le but de ma thèse était de proposer des techniques hybrides issues de ces deux domaines, dans le cadre de la résolution de problèmes et de l'analyse statique. Mon travail s'est inscrit dans le cadre du projet ANR coverif.

Publications

• Automatic Synthesis of Random Generators for Numerically Constrained Algebraic Recursive Types
  Logic-based Program Synthesis and Transformation (LOPSTR 2022)
  Ghiles Ziat, Matthieu Dien, Vincent Botbol, Arnaud Gotlieb, Martin Pépin, Catherine Dubois
• Automated Random Testing of Numerical Constrained Types
  International Conference on Principles and Practice of Constraint Programming (CP2021)
  Ghiles Ziat, Matthieu Dien, Vincent Botbol
• Constraint-based Verification of Formation Control
  IEEE Conference on Decision and Control (CDC2021)
  Julien Alexandre Dit Sandretto, Alexandre Chapoutot, Christophe Garion, Xavier Thirioux, Ghiles Ziat,
• Abstract domains for constraint programming with differential equations
  International Workshop on Numerical and Symbolic Abstract Domains(NSAD2020)
  Ghiles Ziat, Olivier Mullier, Julien Alexandre dit Sandretto, Christophe Garion, Alexandre Chapoutot, Xavier Thirioux
• Combination of Boxes and Polyhedra Abstractions for Constraint Solving
  International Workshop on Numerical and Symbolic Abstract Domains (NSAD2019)
  Ghiles Ziat, Alexandre Maréchal Marie Pelleau, Charlotte Truchet, Antoine Miné
• Finding Solutions by Finding Inconsistencies
  International Conference on Principles and Practice of Constraint Programming(CP2018)
  Ghiles Ziat, Marie Pelleau, Charlotte Truchet, Antoine Miné,
• Améliorer la propagation : l'Importance d'être Inconsistant
  Journées Francophones de Programmation par Contraintes(JFPC2017)
  Ghiles Ziat, Marie Pelleau, Charlotte Truchet, Antoine Miné
• Mixing Polyedra and Boxes Abstract Domain for Constraint Solving
  CP meets Verification Workshop (CPCAV2016)
  Marie Pelleau, Emmanuel Rauzy, Ghiles Ziat, Charlotte Truchet, Antoine Miné,
• These de doctorat: A Combination of Abstract Interpretation and Constraint Programming
  Ghiles Ziat,

Logiciels

Je contribue activement aux logiciels suivants :

• Testify
  est une extension syntaxique pour OCaml qui génére automatiquement des tests
• AbSolute
  Solveur de contraintes basé sur des domaines abstraits : Essayer
• Picasso
  Picasso est une bibliothèque de dessins d'éléments abstraits
• geoml
  Bibliothèque de géométrie 2D en OCaml

Enseignement

Vérification de Programmes en COQ

Semaine 1 : Logiques Booléenne et Propositionnelle

Télécharger le TP (1)

Télécharger le Live Coding (1)

Semaine 2 : Arithmétique, Récurrence, Induction

Télécharger le TP (2)

Télécharger le Live Coding (2)

Semaine 3 : Induction Structurelle, Propositions Inductives

Télécharger le TP (3)

Télécharger le Live Coding (3)

Télécharger le Live Coding (4)

Examen Blanc

Télécharger le fichier de preuves à compléter exam_student.v

Enseignements passés

avant 2022

• Éléments de programmation 1 (1I001)
  L1, Licence de Sciences et Technologies, Mention Informatique, Paris 6 :
• Fonctions et procédures de calcul (2I008)
  L2, Licence de Sciences et Technologies, Mention Informatique, Paris 6 :
• Développement d’un langage de programmation
  M1, Master d'informatique, Spécialité STL, Paris 6 : lien
• Algorithmique et Programmation en C
  1ère année, ISAE-supaero: lien
• Programmation fonctionnelle Théorie des langages/Compilation
  3ème année, ENSEEIHT
• Typage et Analyse Statique
  M2, Master d'informatique, Langages et Programmation, Paris Diderot