Hichem Rami AIT EL HARA
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)