As part of a project funded by the French National Research Agency (ANR), CLEARSY is collaborating with LORIA (Nancy), CRIL (Lens) and the University of Liège to improve the mathematical demonstration tools of Atelier B.
When Atelier B is used to develop secure software, it produces mathematical proof obligations that must then be resolved.
Atelier B’s demonstration tools (provers) already enable a large proportion of these to be resolved automatically.
The project “Enhancing B Language Reasoners with SAT and SMT Techniques” aims to improve the efficiency of these demonstrators.
The initial results are already conclusive!
On a test bench of 681,285 proof obligations, techniques based on SAT-type consistency verification tools and SMT-type consistency checking tools have enabled us to increase the number of automatically proven proof obligations from 74% to 87%.
TARGET: Over 90% by the end of the project in March 2027!