Embedding Formally Proved Code in a Smart Card: Converting B to C. - Antoine Requet; Gaëlle Bossu (ICFEM, 2000)