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, José Fragoso Santos.
To appear in TACAS 2026: 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
[Paper] [HAL]

Theory of sequences tailored for program verification
Hichem Rami Ait-El-Hara.
PhD manuscript, published in Nov 2025.
[Archive] [Manuscript] [Slides] [HAL] [Defense Page]

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]

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]

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] [HAL] [Publisher Version]

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] [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] [HAL] [Publisher Version]

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] [HAL]

TACAS 2026: Artifact Evaluation Committee

FM 2026: Subreviewer

CAV 2025: Artifact Evaluation Committee

TACAS 2025: Artifact Evaluation Committee

SMT workshop 2024: Subreviewer

SMT workshop 2023: Subreviewer

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] [slides (in French)]

Report on GraphCompressor. [pdf]