Sylvain Conchon
Useful informations / Informations utiles
-
Phone/Tél: (+33) (0)1 69 15 65 52
-
Fax : (+33) (0)1 74 85 42 29
-
Address/Adresse:
- LRI, bâtiment 650
- Université Paris-Sud 11
- 91405 Orsay cedex
- France
- Office/Bureau : 36
-
Email/Courriel: Sylvain.Conchon[at]lri.fr
Site web du nouveau
Master
Informatique de Paris-Saclay
I'm Professor at Paris-Sud University and a member of
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-Sud et membre
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 :
- 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
Enseignement
Cette année, je m'occupe des cours suivants:
Livre
Vulgarisation
My PGP key / Ma clé PGP
ici/here
[Eyrolles]
[Amazon]
[Eyrolles]
[Amazon]