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)

Hobbies

I'm a hobbyist genealogist. You can explore my family tree on GeneaNet. Who knows, maybe we are distant cousins ?