Jérome Ricciardi
Méthodes formelles, outils OCaml et logiciel quantique
Je suis ingénieur logiciel et chercheur appliqué, avec une spécialisation en méthodes formelles et en logiciel quantique. Mon travail porte sur le développement d'outils, la vérification de programmes et de circuits, et le support applicatif auprès d’utilisateurs de plateformes de calcul scientifique.
J’ai travaillé sur la vérification déductive, l’exécution symbolique, le développement d’outils en OCaml, et les techniques de vérification pour circuits quantiques et hybrides.
Poste actuel
Application Support Engineer chez Quandela, je travaille sur Lucy, l’ordinateur quantique de Quandela déployé au TGCC. J’ai participé à son intégration dans le centre de calcul. J’accompagne les utilisateurs sur les aspects applicatifs et algorithmiques, et je fais le lien entre Quandela et le TGCC.
Recherche / thèse
J'ai soutenu ma thèse, Vérification pratique des transformations de circuits quantiques, le à l'École normale supérieure Paris-Saclay.
La thèse porte sur la vérification déductive, l'équivalence de circuits quantiques et hybrides, les transformations de circuits et le développement d'outils pour des workflows de vérification formelle.
Documents de thèse
- Manuscrit de thèse (PDF, 2,2 Mo)
- Diapositives de soutenance (PDF, en anglais, 10,7 Mo)
Projets
Projets de thèse
-
Qbricks to OpenQASM
Développement Why3 pour certifier une chaîne de traduction de Qbricks vers OpenQASM. Le travail prouve des réécritures préservant la sémantique, afin d’éliminer ou de compiler certains constructs Qbricks avant la génération de code OpenQASM.
-
SQbricks
Chaîne d’outils pour vérifier automatiquement des transformations de circuits quantiques hybrides. Elle combine le lifting par deferred measurement avec des vérifications d’équivalence sur les sorties observées et de séparation, afin de traiter les mesures, le contrôle classique et les données discardées.
Projets de master
-
AutoCheck
Projet de master sur le test automatisé et la vérification de propriétés OCaml et WhyML.
-
ENUM
Projet de master lié au test par énumération et à la vérification de propriétés.
Quandela / travaux liés
-
Reproduced papers
Dépôt associé à MerLin pour la reproduction et le benchmark de papiers publiés en quantum machine learning, avec un focus sur le calcul quantique photonique et hybride. Il fournit du code réutilisable, des notebooks et des ressources d’analyse pour comparer les résultats reproduits.
Articles
-
Towards random and enumerative testing for OCaml
and WhyML properties
Clotilde Erard, Jérome Ricciardi, Alain Giorgetti. Software Quality Journal, 2022. DOI : 10.1007/s11219-021-09572-z.
-
Quantum Circuit Equivalence Checking: A Tractable
Bridge From Unitary to Hybrid Circuits
Jérome Ricciardi, Sébastien Bardin, Christophe Chareton, Benoît Valiron. arXiv:2511.22523, 2025.
Compétences
- OCaml
- Vérification formelle
- Vérification déductive
- Exécution symbolique
- Circuits quantiques
- Logiciel quantique
- Développement d'outils
- Python
- Git
- Linux
