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.
Enseignements
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 |
Contact
La Chantrerie
4, rue Alfred Kastler - B.P. 20722
F-44307 NANTES Cedex 3
Phone: (33) 2 76 64 51 87
Office at IMT: B210
Office at Faculty: LS2N, n°117