What is B4Free ?
B4free is a set of tools for the development of B models.
B4Free, is the single-user version of Atelier
B with the capability of generating code C with ComenC translator. Components are limited to 4000 proof
obligations.
B4Free is mainly aimed at the university academic environment but
also anyone wishing to become initiated into B tools.