BLaSST project

Enhancing B Language Reasoners Using SAT and SMT Techniques

About BLaSST

BLaSST is a project funded by ANR, the French research agency. It involves the VeriDis team of Inria in Nancy, the CRIL laboratory of University of Artois in Lens, the CLEARSY company, and the Montefiore Institute of University of Liège in Belgium. BLaSST was selected for funding as project ANR-21-CE25-0010.

The project started in March 2022 and runs until February 2027.

Executive summary

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 investigated. 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.

Pages