The B method takes up floating-point numbers

International audienceFor a long time, formal methods have ignored floating-point computations. About ten years ago this has changed, and today specification languages and tools are in use in research and pre-industrial contexts. Better late than never: the B method, which has been the first formal method to prove real-size software, will soon be able to prove the correctness of floating-point computations. This paper gives the motivations, the philosophy and the first impacts on the AtelierB tool