About
I'm an R&D engineer at OCamlPro, a company specialized in OCaml developments and formal methods. Before this, I was a PhD student at Laboratoire de Recherche en Informatique and teaching assistant at IUT d'Orsay. My thesis is about verification of concurrent programs on weak memory models via model checking techniques. In particular, I worked on Cubicle-W, an extension of the Cubicle model checker that adds support for weak memory models, and its applications.
Tool pages
Cubicle-W:
an extension of Cubicle for weak memory
PMCx86: an application that translates x86 assembly
programs to Cubicle-W
Publications
Parameterized Model Checking on the TSO Weak Memory Model
Sylvain Conchon, David Declerck and Fatiha Zaïdi
In Journal of Automated Reasoning, Volume 64, 2020
Vérification par model-checking de programmes concurrents
paramétrés sur des modèles mémoires faibles
Ph.D. Thesis (in french),
Université Paris-Sud, Orsay, September 2018
Cubicle-W: Parameterized Model Checking on Weak Memory
Sylvain Conchon, David Declerck and Fatiha Zaïdi
In Ninth International Joint Conference on Automated Reasoning,
Oxford, United Kingdom, July 2018
Parameterized Model Checking Modulo
Explicit Weak Memory Models
Sylvain Conchon, David Declerck and Fatiha Zaïdi
In First International Workshop on Handling IMPlicit and EXplicit
knowledge in formal system development,
Xi'an, China, November 2017
Compiling Parameterized x86-TSO Concurrent Programs to
Cubicle-W
Sylvain Conchon, David Declerck and Fatiha Zaïdi
In 19th International Conference on Formal Engineering Methods,
Xi'an, China, November 2017
Vérification de programmes assembleur
concurrents sur modèle mémoire x86-TSO
Master's degree internship report (in french),
Université Paris-Sud, Orsay, September 2014
Vérification de programmes C concurrents
avec Cubicle : Enfoncer les barrières
Sylvain Conchon, David Declerck, Luc Maranget and Alain Mebsout
In Vingt-Cinquièmes Journées Francophones des Langages Applicatifs,
Fréjus, France, January 2014
Teachings
IUT Orsay - 2014-2017 - | Principes des systèmes d'exploitation (S3) |
Algorithmique Avancée (S3) | |
Conception et Programmation Orientée Objet (S3) | |
Architecture et programmation des mécanismes de base d'un système informatique (S2) | |
Projet Personnel et Professionnel (S1) |
Responsibilities
EDIPS - Ph.D. students representative (2014-2015) |
ED STIC - Ph.D. students representative (2014-2015) |