Hichem Rami AIT EL HARA

Publications

2026

  • colibri2: A CP solver for SMT problems Preprint
    François Bobot, Hichem Rami Ait-El-Hara, and Bruno Marre.
    Paper HAL 

    @unpublished{bobot:cea-05644448,
  TITLE = {{colibri2: A CP solver for SMT problems}},
  AUTHOR = {Bobot, Fran{\c c}ois and Ait El Hara, Hichem Rami and Marre, Bruno},
  URL = {https://cea.hal.science/cea-05644448},
  NOTE = {working paper or preprint},
  YEAR = {2026},
  MONTH = Mar,
  KEYWORDS = {CP solver ; SMT solver ; scheduling ; propagation ; domains 1},
  PDF = {https://cea.hal.science/cea-05644448v1/file/paper.pdf},
  HAL_ID = {cea-05644448},
  HAL_VERSION = {v1},
}

  • 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, Petar Maksimović, Nuno Santos, and José Fragoso Santos.
    TACAS @ ETAPS 2026: Tools and Algorithms for the Construction and Analysis of Systems: 32nd International Conference, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026.
    Paper Publisher Version HAL 

    @inproceedings{10.1007/978-3-032-22752-2_2,
  author    = {Pereira, Jo{\~a}o Madeira and Marques, Filipe and Ad{\~a}o, Pedro and Ait-El-Hara, Hichem Rami and Andr{\`e}s, L{\'e}o and Carcano, Arthur and Chambart, Pierre and Maksimovi{\'c}, Petar and Santos, Nuno and Santos, Jos{\'e} Fragoso},
  title     = {Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml},
  year      = {2026},
  isbn      = {978-3-032-22751-5},
  publisher = {Springer-Verlag},
  address   = {Berlin, Heidelberg},
  url       = {https://doi.org/10.1007/978-3-032-22752-2_2},
  doi       = {10.1007/978-3-032-22752-2_2},
  abstract  = {SMT solvers are essential for applications in artificial intelligence, software verification, and optimisation. However, no single solver excels across all formula types, and different applications may require the use of different solvers. While the SMT-LIB language enables multi-solver support, it also incurs heavy I/O overhead. To address this, we introduce Smt.ml, an SMT-solver frontend for OCaml that simplifies integration with various solvers through a consistent interface. Its parametric encoding facilitates the easy addition of new solver backends, while optimisations like formula simplification, result caching, and detailed error feedback enhance performance and usability. Furthermore, Smt.ml is the only SMT frontend that includes a simplification-management engine for streamlining the integration of new formula simplifications and the verification of their correctness. Our evaluation demonstrates that Smt.ml ’s results are consistent with those of its backend solvers and that its optimisations are highly effective on formulas generated from the symbolic execution of an extensive program-analysis benchmark.},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems: 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11–16, 2026, Proceedings, Part I},
  pages     = {23–44},
  numpages  = {22},
  keywords  = {SMT Solvers, Symbolic Execution, OCaml, SMT-LIB},
  location  = {Turin, Italy}
}

2025

  • Theory of Sequences Tailored for Program Verification
    Hichem Rami Ait-El-Hara.
    PhD manuscript, published in Nov 2025.
    Archive Manuscript Slides HAL Defense Page 

    @phdthesis{aitelhara:tel-05383515,
  title       = {{Theory of sequences tailored for program verification}},
  author      = {Ait El Hara, Hichem Rami},
  url         = {https://theses.hal.science/tel-05383515},
  number      = {2025UPASG067},
  school      = {{Universit{\'e} Paris-Saclay}},
  year        = {2025},
  month       = Oct,
  keywords    = {Constraint programming ; Constraint solver ; Satisfiability Modulo Theories ; SMT solver ; Theory of sequences ; Program verification ; Programmation par contraintes ; Solveur de contraintes ; Satisfibilit{\'e} Modulo Th{\'e}ories ; Solveur SMT ; Th{\'e}orie des s{\'e}quences ; V{\'e}rification de programmes},
  type        = {Theses},
  pdf         = {https://theses.hal.science/tel-05383515v1/file/151738_AITELHARA_2025_archivage.pdf},
  hal_id      = {tel-05383515},
  hal_version = {v1}
}

  • Reasoning over n-Indexed Sequences in SMT
    Hichem Rami Ait-El-Hara, François Bobot, and Guillaume Bury.
    Acta Informatica — Selected Extended Papers of SMT 2024 and Related Papers.
    Paper Publisher Version 

    @article{ait-el-hara_acta_2025,
  author  = {Ait-El-Hara, Hichem Rami
             and Bobot, Fran{\c{c}}ois
             and Bury, Guillaume},
  title   = {Reasoning over n-indexed sequences in SMT},
  journal = {Acta Informatica},
  year    = {2025},
  month   = {Aug},
  day     = {21},
  volume  = {62},
  number  = {3},
  pages   = {33},
  issn    = {1432-0525},
  doi     = {10.1007/s00236-025-00496-w},
  url     = {https://doi.org/10.1007/s00236-025-00496-w}
}

  • Constraint Propagation for Bit-Vectors in Alt-Ergo
    Hichem Rami Ait-El-Hara, Guillaume Bury, Basile Clément and Pierre Villemot.
    SMT 2025: 23rd International Workshop on Satisfiability Modulo Theories.
    Paper Publisher Version 

    @inproceedings{ait-el-hara_constraint_2025,
  address   = {Glasgow, UK},
  series    = {{CEUR} {Workshop} {Proceedings}},
  title     = {Constraint {Propagation} for {Bit}-{Vectors} in {Alt}-{Ergo}},
  volume    = {4008},
  url       = {https://ceur-ws.org/Vol-4008/#SMT_paper20},
  language  = {en},
  urldate   = {2025-08-15},
  booktitle = {Joint {Proceedings} of the 23rd {International} {Workshop} on {Satisfiability} {Modulo} {Theories} and the 16th {Pragmatics} of {SAT} {International} {Workshop}},
  publisher = {CEUR},
  author    = {Ait-El-Hara, Hichem Rami and Bury, Guillaume and Cl{\'e}ment, Basile and Villemot, Pierre},
  editor    = {Hoenicke, Jochen and Janota, Mikol{\'a}{\v s} and Niemetz, Aina and Tourret, Sophie},
  month     = aug,
  year      = {2025},
  note      = {ISSN: 1613-0073},
  pages     = {65--76}
}

  • Relational Abstractions Based on Labeled Union-Find
    Dorian Lesbre, Matthieu Lemerre, Hichem Rami Ait-El-Hara, and François Bobot.
    PLDI 2025: 46th ACM SIGPLAN Conference on Programming Language Design and Implementation.
    Paper Publisher Version HAL 

    @article{10.1145/3729298,
  author     = {Lesbre, Dorian and Lemerre, Matthieu and Ait-El-Hara, Hichem Rami and Bobot, Fran\c{c}ois},
  title      = {Relational Abstractions Based on Labeled Union-Find},
  year       = {2025},
  issue_date = {June 2025},
  publisher  = {Association for Computing Machinery},
  address    = {New York, NY, USA},
  volume     = {9},
  number     = {PLDI},
  url        = {https://doi.org/10.1145/3729298},
  doi        = {10.1145/3729298},
  abstract   = {We introduce a new family of abstractions based on a data structure that we call labeled union-find, an extension of the classic efficient union-find data structure where edges carry labels. These labels have a composition operation that obey the group axioms. Like union-find, the labeled version can efficiently compute the transitive closure of a relation, but it is not limited to equivalence relations; it can represent any injective transformation between equivalence classes, which includes two-variables per equality (TVPE) constraints of the form y = a\texttimes{} x + b. Using abstract interpretation theory, we study the properties deriving from the use of abstract relations as labels, and the combination of labeled union-find with other representations of constraints, allowing both improvements in precision and simplification of existing constraints. Due to its efficiency, the labeled union-find abstractions could find many uses; we use it in two use cases, program analysis based on abstract interpretation and constraint solving for SMT, with encouraging preliminary results.},
  journal    = {Proc. ACM Program. Lang.},
  month      = jun,
  articleno  = {195},
  numpages   = {26},
  keywords   = {Abstract interpretation, Labeled union-find, Relational abstract domain}
}

2024

  • 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 Publisher Version HAL 

    @inproceedings{ait_el_hara_smt24,
  title     = {An {SMT} {Theory} for n-{Indexed} {Sequences}},
  author    = {Ait-El-Hara, Hichem Rami and Bobot, Fran{\c c}ois and Bury, Guillaume},
  booktitle = {Proceedings of the 22nd {International} {Workshop} on {Satisfiability} {Modulo} {Theories}},
  editor    = {Reger, Giles and Zohar, Yoni},
  series    = {{CEUR} {Workshop} {Proceedings}},
  volume    = {3725},
  publisher = {CEUR},
  issn      = {1613-0073},
  url       = {https://ceur-ws.org/Vol-3725/#short13},
  pages     = {64--74},
  address   = {Montreal, Canada},
  month     = jul,
  year      = {2024},
  language  = {en}
}

  • 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 Publisher Version HAL 

    @inproceedings{ait_el_hara_lpar24,
  title     = {On {SMT} {Theory} {Design}: {The} {Case} of {Sequences}},
  author    = {Ait-El-Hara, Hichem Rami and Bobot, Fran{\c c}ois and Bury, Guillaume},
  booktitle = {LPAR 2024 Complementary Volume},
  editor    = {Nikolaj Bjørner and Marijn Heule and Andrei Voronkov},
  series    = {Kalpa Publications in Computing},
  volume    = {18},
  publisher = {EasyChair},
  issn      = {2515-1762},
  url       = {https://easychair.org/publications/paper/qdvJ},
  doi       = {10.29007/75tl},
  pages     = {14--29},
  month     = may,
  year      = {2024},
  language  = {en}
}

2022

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

    @inproceedings{ait_el_hara_jfla22,
  title     = {{Alt-Ergo-Fuzz}: {A} fuzzer for the {Alt-Ergo} {SMT} solver},
  author    = {Ait-El-Hara, Hichem Rami and Bury, Guillaume and de Oliveira, Steven},
  booktitle = {{33{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs}},
  editor    = {Chantal Keller and Timothy Bourke},
  url       = {https://inria.hal.science/hal-03626861},
  pages     = {235--244},
  address   = {Saint-M{\'e}dard-d'Excideuil, France},
  month     = jun,
  year      = {2022},
  pdf       = {https://inria.hal.science/hal-03626861v1/file/jfla22_paper_15.pdf},
  language  = {en}
}

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 (in French). PDF Slides

  • Report on GraphCompressor. Report Source

ORCIDLinkedInGoogle ScholarGitHub