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.