Augustin Lesage painting (artist from my hometown)

Constraint Programming for Verification

Under supervision of Prof. Éric Monfroy and Dr. Charlotte Truchet .

I started my PhD at Institut Mines-Télécom Atlantique in September, 2014 into the Laboratoire des Sciences du Numérique de Nantes (LS2N) inside the Théorie, Algorithmes et Systèmes en Contraintes (TASC) team. I focus on solving verification problems using constraint programming.

As a first application, we started with FAUST, which is a real-time language designed by the GRAME in Lyon for processing and generating audio streams. This language is similar to other real-time languages such as Lustre or Esterel. Given a program, we were interested to compute relevant bounds for all the variables in it.

Lastly, we considered models generalizing Markov chains and we used constraint programming to prove properties on such objects. This can be applied for modeling systems in which probabilities play a fundamental role, such as randomized protocols, biological systems, and also economics or finance.



Tous réalisés à l'Institut Mines-Télécom sur Nantes.

Module Formation Enseignement
Algorithmie et programmation en Java 1A cycle ingénieur TD/TP
Structures algorithmiques 1A cycle ingénieur TD/TP
Projet de programmation informatique 1A cycle ingénieur Encadrement
Ingénierie logicielle et programmation objet 2A cycle ingénieur CM/TD/TP


Institut Mines-Télécom Atlantique
La Chantrerie
4, rue Alfred Kastler - B.P. 20722
F-44307 NANTES Cedex 3

E-mail: contact
Phone: (33) 2 76 64 51 87
Office at IMT: B210
Office at Faculty: LS2N, n°117