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


  • 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