Publications
2026
-
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
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
-
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
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 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
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 HAL