M. Barbosa, J. Pinto, J.-C. Filliatre, and B. Vieira, “A Deductive Verification Platform for Cryptographic Software”, eceasst, vol. 33, Dec. 2010.