Curriculum vitæ


2017: Ph.D. - Operational Research (Artificial Intelligence)
              Institut Mines Télécom Atlantique (France)

2014: Master Degree - Web Development
              Université d'Artois (France)

2014: Master Degree - Artificial Intelligence
              Université d'Artois (France)

📷 crédit : Jean-Dominique Billaud/LVAN

Constraint modelling and solving of some verification problems

Supervisors: Éric Monfroy, Charlotte Truchet, Benoît Delahaye

Astract : Constraint programming offers efficient languages andtools for solving combinatorial and computationally hard problems such as the ones proposed in program verification. In this thesis, we tackle two families of program verification problems using constraint programming.In both contexts, we first propose a formal evaluation of our contributions before realizing some experiments.The first contribution is about a synchronous reactive language, represented by a block-diagram algebra. Such programs operate on infinite streams and model real-time processes. We propose a constraint model together with a new global constraint. Our new filtering algorithm is inspired from Abstract Interpretation. It computes over-approximations of the infinite stream values computed by the block-diagrams. We evaluated our verification process on the FAUST language (a language for processing real-time audio streams) and we tested it on examples from the FAUST standard library. The second contribution considers probabilistic processes represented by Parametric Interval Markov Chains, a specification formalism that extends Markov Chains. We propose constraint models for checking qualitative and quantitative reachability properties. Our models for the qualitative case improve the state of the art models, while for the quantitative case our models are the first ones. We implemented and evaluated our verification constraint models as mixed integer linear programs and satisfiability modulo theory programs. Experiments have been realized on a PRISM based benchmark.


See full list of publications and citations on dblp and Google Scholar.