Naïm Moussaoui Remil

PhD Candidate in Computer Science

École Normale Supérieure | PSL · Inria Paris · Paris, France

dblp
News! latest updates
  • Feb 2026 Invited talk Termination Resilience Static Analysis at the LACL Seminar, Université Paris-Est Créteil.
  • Jan 2026 Presented Termination Resilience Static Analysis at VMCAI 2026, Rennes.
  • 2026 New competition contribution: ReFuncTion tool demo accepted at TACAS 2026 / SV-COMP (ETAPS).
  • Nov 2025 Talk Static Program Analysis Across Trust Boundaries at the iFM 2025 PhD Symposium, Paris.
  • Oct 2025 Invited to Dagstuhl Seminar 25421 — Sound Static Program Analysis in Modern Software Engineering, Schloss Dagstuhl.

About

Portrait of Naïm Moussaoui Remil

Expertise

#Formal-Methods #Verification #Static-Analysis #Abstract-Interpretation #Temporal-Properties #Software-Security

Curriculum Vitæ

Download CV (PDF)

I am a PhD candidate in Computer Science at the École Normale Supérieure (PSL) and Inria Paris, supervised by Caterina Urban (ENS & Inria).

My research focuses on providing mathematical guarantees about program behavior. I explore the verification of temporal properties of sequential C-like programs. Specifically, I use abstract interpretation to develop static analyses proving CTL properties of programs in adversarial contexts, including termination resilience and vulnerable variable detection.

My PhD topic is Static Analysis by Abstract Interpretation for CTL Properties in Adversarial Contexts.

More broadly, I aim to generalize this branching-time setting (CTL) to Alternating-time Temporal Logic (ATL), which captures what an agent can guarantee against an adversary. This unifies the problems I study — termination resilience and vulnerable variable detection — as strategic temporal properties, all provable within a single sound abstract-interpretation framework for C-like numerical programs.

Publications

Google Scholar →
2026

Termination Resilience Static Analysis

Naïm Moussaoui Remil, Caterina Urban

VMCAI 2026 PDF Artifact DOI

ReFuncTion: Conditional Termination by Abstract Interpretation of Numerical C Programs (Competition Contribution)

Naïm Moussaoui Remil, Caterina Urban

TACAS 2026 PDF DOI
2024

Automatic Detection of Vulnerable Variables for CTL Properties of Programs

Naïm Moussaoui Remil, Caterina Urban, Antoine Miné

LPAR 2024 PDF Artifact DOI

Experience & Education

Research Experience

Research Intern — M2

2023

Inria Paris, Équipe Antique — ENS, Paris

Vulnerable variable detection for CTL properties by abstract interpretation (Caterina Urban & Antoine Miné). Led to LPAR 2024 and to the PhD.

Research Intern — M1

2022

MPI-SWS, Kaiserslautern, Germany

Extending the GenMC model-checker (Viktor Vafeiadis).

Research Intern

2021–22

ENS de Rennes, France

9-month research project (Martin Quinson & Thierry Jéron).

Research Intern — L3

2021

LACL, Université Paris-Est Créteil, France

Visualising global graph transformation (Antoine Spicher).

Education

PhD in Computer Science

2023–present

Inria Paris & ENS | PSL

Master 2 — MPRI

2022–23

ENS Paris · Polytechnique · Paris-Cité · ENS Paris-Saclay

Normalien Élève — CS (Master)

2019–23

ENS de Rennes (admitted via second concours)

Double Major BSc — Maths & CS

2017–19

Université Paris-Est Créteil — summa cum laude

Teaching

Teaching Assistant (Chargé de TD)

2024–25

ENS | PSL, Paris

Practical sessions for second-year CPES students, including Lustre synchronous programming.

Teaching Assistant — C Programming

2024–25

Sorbonne Université, Paris

Practical sessions in C programming.

Academic Service

  • Sub-reviewer, OOPSLA2026
  • Sub-reviewer, SAS2026
  • Artifact Evaluation Committee, SAS / SPLASH2024

Talks & Seminars

Invited Talks

  • Termination Resilience Static Analysis

    LACL Seminar, Université Paris-Est Créteil — Feb 2026

  • Static Program Analysis Across Trust Boundaries

    Dagstuhl Seminar 25421, Schloss Dagstuhl — Oct 2025

  • Termination Resilience Static Analysis

    SemAntique, Inria/Antique, Paris — Mar 2025

  • Termination Resilience Static Analysis by Abstract Interpretation

    Inria PhD Seminar, Paris — Mar 2025

  • Automatic Detection of Vulnerable Variables for CTL Properties

    SemAntique, Inria/Antique, Paris — Mar 2024

Conferences & Symposia

  • Termination Resilience Static Analysis

    VMCAI 2026, Rennes — Jan 2026

  • ReFuncTion: Conditional Termination by Abstract Interpretation (Tool Demo, SV-COMP)

    TACAS 2026, ETAPS

  • Static Program Analysis Across Trust Boundaries

    iFM 2025 PhD Symposium, Paris — Nov 2025

  • Automatic Detection of Vulnerable Variables for CTL Properties

    LPAR 2024, Port Louis, Mauritius — May 2024

Open-Source Software

FuncTion / FuncTion-V / ReFuncTion

Abstract-interpretation-based static analyzer for (conditional) alternating-time temporal properties — including classical termination, non-termination and CTL properties — of C-like numerical programs. Written in OCaml. Extension of FuncTion by Caterina Urban.

Marsh

A small language for probabilistic programming with exact inference. Written in OCaml.

Technical Skills

Languages
OCaml, Python, C, Rust, Bash, HTML/CSS, JavaScript, Lustre
Formal Methods
Abstract Interpretation, Static Analysis, Temporal Specification, Program Logic, Taint Analysis, Software Security, Synchronous Programming
Tools
Git, LaTeX, Linux
Spoken
French (native), English (fluent)