ANR has selected the project BLaSST (Enhancing B Language Reasoners with SAT and SMT Techniques) under the framework “appel à projets générique 2020”.
- DURATION : 48 months
- PARTNERS: INRIA Nancy (leader), CLEARSY, CRIL Lens, Université de Liège
The BLaSST project targets bridging combinational and symbolic techniques in automatic theorem proving and validating the results for proof obligations generated from B models.
Work will be carried out on SAT-based encodings and optimized resolution techniques for proof, model generation, and lemma suggestion, as well as on encoding and reasoning techniques for expressive SMT-based formalisms.
Combining both lines of work, the expected scientific impact is an increase of the automation of solvers for expressive input languages by leveraging higher-order reasoning and enumerative instantiations for quantifiers over finite domains.
The effectiveness of the techniques will be quantified by validation over industrial benchmarks that are known to be difficult for current reasoning engines. The industrial impact of BLaSST will be higher productivity of proof engineers. The benchmarks and improved solvers will be made openly available under permissive open-source licenses.
