Yakoub SALHI

Full Professor of Computer Science

Université d'Artois

Centre de Recherche en Informatique de Lens



Research Activities

My research activities are mainly concerned with artificial intelligence (AI), and more specifically with automated reasoning, knowledge representation, formal logics and data mining.

Recent Publications

Current Projects


This is a joint project with INRIA Nancy (PI), ULiège and Clearsy.

The BLaSST project targets bridging combinatorial and symbolic techniques in automatic theorem proving, in particular for proof obligations generated from B models. It focuses on advancing the state of the art in automated reasoning, in particular SAT and SMT techniques, and on making these techniques available to software verification. More specifically, encoding techniques, optimized resolution techniques, model generation, and lemma suggestion will be considered. The expected scientific impact is a substantially higher degree of automation of solvers for expressive input languages by leveraging higher-order reasoning and enumerative instantiations over finite domains, as well as useful feedback for verification conditions that cannot be proved. The effectiveness of the techniques developed in the project will be quantified by applying them to benchmark sets provided by the industrial partner. The industrial impact of BLaSST will be a higher productivity of proof engineers. The collections of benchmarks and the reasoning engines will be made openly available under permissive open-source licenses.