Enhancing B Language Reasoners with SAT and SMT Techniques – BLaSST

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.