Sylvain Conchon
Useful informations / Informations utiles
I'm Professor at Paris-Saclay University and a member
of LMF (the Formal Methods
Laboratory - ULMR 9061) and the Toccata team, a joint
project with
INRIA Saclay -
Île-de-France. Previously, I was Senior Research Associate
in the OBASCO
team at Ecole des Mines de Nantes, Senior Research Associate in
the PacSoft team at
the OGI School of Science & Engineering at OHSU and Ph.D student
at INRIA Rocquencourt in
the MOCSOVA team.
Je suis Professeur à l'Université Paris-Saclay, membre
du LMF (Laboratoire Méthodes Formelles - UMR
9021) et de
l'équipe Toccata
commune à INRIA Saclay -
Île-de-France. Avant cela, j'étais chercheur invité dans
l'équipe OBASCO
de l'Ecole des Mines de Nantes, chercheur associé dans
l'équipe PacSoft de
l'OGI School of Science & Engineering at OHSU et étudiant en
thèse dans le
projet Moscova à l'INRIA
Rocquencourt.
Research / Recherche
My
habilitation
thesis is about SMT (satisfiability modulo theory)
techniques and their
applications. My PhD thesis
(in french) is about information flow analysis for functional
and concurrent programming languages.
I'm currently working on automated deduction for program
verification and model checking for parameterized systems.
Here is a list of
my publications.
Le thème de
ma thèse
d'habilitation porte sur les techniques SMT (satisfiabilité
modulo théorie) et leurs applications. Le thème de
ma thèse de doctorat est
l'analyse de flot d'information dans les langages de
programmation fonctionnels et concurrents.
Je travaille actuellement dans le domaine de la démonstration
automatique pour la preuve de programmes et le model checking
pour systèmes paramétrés.
Voici une liste de mes publications.
Research projects:
Conferences : I was (or I am) involved in the
organisation of the following conferences
Doctoral juries :
- Lucas Massoni Sguerra, PhD, Contrats
intelligents pour les enchères : de l'évaluation expérimentale à
la confidentialité, Université PSL, 19 Avr. 2023
(Reviewer)
- David Nizard, PhD, Programmation mathématique
non convexe non linéaire en variables entières : un exemple
d'application au problème de l'écoulement de larges blocs
d'actifs, Université Paris Saclay, 12 Avr. 2023
(Examiner)
- Guillaume Girol, PhD, Robust reachability
and model counting for software security, Université Paris
Saclay, 17 Oct. 2022 (Advisor)
- Lulu He, PhD, Formal verification at design
stage of diagnosis related properties for discrete event and
real-time systems, Université Paris Saclay, 18 Mai 2022
(Examiner)
- Natkamon Tovanich, PhD, Visual Analytics for
Monitoring and Exploration of Bitcoin Blockchain Data,
Université Paris Saclay, 8 Fev. 2022 (Examiner)
- Martin Morterol, PhD, Méthodes avancées de
raisonnement en logique propositionnelle : application aux réseaux
métaboliques, Université Paris Saclay, 13 Dec. 2016
(Examiner)
-
Allan Blanchard, PhD, Aide à la vérification de
programmes concurrents par transformation de code et de
spécifications, Université d'Orléans, 6 Dec. 2016
(Reviewer)
-
Xavier Thirioux, HDR, Verifying Embedded
Systems, Institut National Polytechnique de Toulouse, 19
Sept. 2016 (Reviewer)
-
Laurent Cabaret, PhD, Algorithmes d'étiquetage en
composantes connexes efficaces pour architectures hautes
performances, Université Paris Saclay, 28 Sept. 2016
(Examiner)
-
Lourdes del Carmen Gonz\'alez
Huesca, PhD, Incrementality and Effect Simulation in
the Simply Typed Lambda Calculus, Université Paris Diderot, 27
Nov 2015(Reviewer)
- Kailiang Ji, PhD, Model Checking and Theorem
Proving, Université Paris Diderot, 25 Sept. 2015 (Reviewer)
- Simon Cruanes, PhD, Extending Superposition
with Integer Arithmetic, Structural Induction, and Beyond, École
Polytechnique, 10 Sept. 2015 (Examiner)
- Stéphane Graham-Lengrand, HDR, Polarities &
Focusing : A journey from Realisability to Automated Reasoning,
Université Paris-Sud, 17 Dec. 2014 (Examiner)
- Cagdas Bozman, PhD, Profilage mémoire
d'applications OCaml, ENSTA, 16 Dec. 2014 (Reviewer)
- Hernan Vanzetto, PhD, Proof automation and type
synthesis for set theory in the context of TLA+, Université de
Lorraine, 8 Dec. 2014 (Reviewer)
- Joël Falcou, HDR, Sofware Abstractions for
Parallel Architectures, Université Paris-Sud, 1 Dec. 2014
(Examiner)
- Chen Wang, PhD, Variants of Deterministic and
Stochastic Nonlinear Optimization Problems , Université
Paris-Sud, 31 Oct. 2014 (Examiner)
- Alain Mebsout, PhD, Inférence d'invariants
pour le model checking de systèmes paramétrés, Université Paris-Sud, 29
Sept. 2014 (Advisor)
- Michael Kruse, PhD, Lattice
QCD Optimization and Polytopic Representations of Distributed
Memory, Université Paris-Sud, 26 Sept. 2014 (Examiner)
- Xiaoping Che, PhD, Cross-Fertilizing Formal
Approaches for Conformance and Performance Testing, Télécom
SudParis, 26 Jun. 2014 (Examiner)
- Pierre Esterie, PhD, Multi-Architectural
Support: A Generic and Generative Approach, Université Paris-Sud, 20
Jun. 2014 (Examiner)
- Mahfuza Farooque, PhD, Automated Reasoning
Techniques as Proof-Search in Sequent Calculus, École
Polytechnique, 19 Dec. 2013 (Reviewer)
- Jianqiang Cheng, PhD, Université Paris-Sud, 8
Nov. 2013 (Examiner)
- Léonard Gérard, PhD, Programmer le parallélisme
avec des futures en Heptagon un langage synchrone flot de données et
étude des réseaux de Kahn en vue d'une compilation synchrone,
Université Paris-Sud, 25 Sept. 2013 (Examiner)
- Mohamed Iguernelala, PhD, Strengthening the
Heart of an SMT Solver: Design and Implementation of Efficient
Decision Procedures, Université Paris-Sud, 10
Jun. 2013 (Advisor)
- Stéphane Lescuyer, PhD, Formalisation et
développement d'une tactique réflexive pour la démonstration
automatique en Coq, Université Paris-Sud, 4 Jan. 2011
(Advisor)
Programming / Tools
- Cubicle : An SMT-based model
checker for parametrized systems
- Alt-Ergo:
An automatic theorem prover dedicated to program verification
-
ocamlgraph: an ocaml graph library
Enseignements 2024/2025
Anciens cours
Livre
- Je suis co-auteur du livre Informatique MP2I/MI : CPGE
1re et 2e années, cours et exercices corrigés.
[Ellipses]
[Amazon]
- Je suis co-auteur du livre Numérique et Sciences
Informatiques, 24 leçons avec exercices
corrigés. Terminale.
[Ellipses]
[Amazon]
- Je suis co-auteur du livre Numérique et Sciences
Informatiques, 30 leçons avec exercices
corrigés. Première.
[Ellipses]
[Amazon]
- Je suis co-auteur du livre Apprendre à
programmer avec OCaml : Algorithmes et structures de
données
[Eyrolles]
[Amazon]
- Je suis co-auteur du livre Informatique pour
tous en classes préparatoires aux grandes écoles: Manuel
d'algorithmique et programmation structurée avec Python
[Eyrolles]
[Amazon]
Vulgarisation
My PGP key / Ma clé PGP
ici/here