Hichem Rami AIT EL HARA

ORCID iD icon https://orcid.org/0000-0001-7909-0413

(To be cited as: "Hichem Rami {Ait El Hara}" or "Ait El Hara, Hichem Rami")

R&D Engineer at OCamlPro, PhD student at Université Paris-Saclay, CEA, List. Mainly working on SMT solving and constraint programming for program verification with a particular focus on the theories of arrays and sequences.

Professional experience

  • PhD student at Université Paris-Saclay, CEA, List, since Sep 2022.
  • R&D Engineer at OCamlPro, since Sep 2021.
  • Research internship at OCamlPro, from Mar 2021 to Sep 2021.

Publications

  • An SMT Theory for n-Indexed Sequences
    Hichem Rami Ait El Hara, François Bobot, and Guillaume Bury.
    SMT 2024: 22nd International Workshop on Satisfiability Modulo Theories.
    [Paper] [BibTex] [HAL] [Publisher Version]

  • On SMT Theory Design: The Case of Sequences
    Hichem Rami Ait El Hara, François Bobot, and Guillaume Bury.
    LPAR 2024: 25th Conference On Logic For Programming, Artificial Intelligence and Reasoning.
    [Paper] [BibTex] [HAL] [Publisher Version]

  • Alt-Ergo-Fuzz: A fuzzer for the Alt-Ergo SMT solver
    Hichem Rami Ait El Hara, Guillaume Bury, Steven de Oliveira.
    JFLA 2022: 33èmes Journées Francophones des Langages Applicatifs.
    [Paper] [BibTex] [HAL]

Preprints

  • Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml
    João Madeira Pereira, Filipe Marques, Pedro Adão, Hichem Rami Ait El Hara, Léo Andrès, Arthur Carcano, Pierre Chambart, Nuno Santos, José Fragoso Santos.
    [Paper] [BibTex] [HAL]

Service

  • TACAS 2025: Artifact Evaluation Committee
  • SMT workshop 2024: Subreviewer
  • SMT workshop 2023: Subreviewer

Education

  • Master's degree in computer science from Sorbonne University, Sep 2021.
    • Title: Software Science and Technology (Fr: STL - Science et Technologie du Logiciel), R&D branch, Software safety and reliability thematic.
    • Main subjects: Algorithmics, Formal methods, Type checking, Static analysis, Program verification, Operational semantics and Process algebras.
  • Bachelor's degree in computer science from Sorbonne University, Sep 2019.

Reports

  • Functional specification and code audit of the Everlend (Ex: Everscalend) DEFI (DEcentralized FInance) lending protocol deployed on the Everscale blockchain. (pdf)
  • Master's thesis. (pdf and slides in French)
  • Report on GraphCompressor. (pdf)