J. Bloch, Nearly all binary searches and mergesorts are broken, 2006.

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., The Astrée static analyzer http

L. Cordeiro, B. Fischer, and J. Marques-silva, SMT-based bounded model checking for embedded ANSI-C software, Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering. ASE '09, pp.137-148, 2009.

H. Tuch, G. Klein, and M. Norrish, Types, bytes, and separation logic, Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07), pp.97-108, 2007.

J. C. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

N. G. De-bruijn, Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Proc. of the Koninklijke Nederlands Akademie, pp.380-392, 1972.

D. Littlewood and A. Richardson, Group Characters and Algebra. Philosophical transactions of the Royal Society of London: Mathematical and physical sciences, 1934.
DOI : 10.1098/rsta.1934.0015

F. Bobot, J. C. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

J. C. Filliâtre, One Logic to Use Them All, 24th International Conference on Automated Deduction, pp.1-20, 2013.
DOI : 10.1007/978-3-642-38574-2_1

J. C. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, 26th International Conference on Computer Aided Verification, pp.1-16, 2014.

G. M. Adel-'son-vel-'ski?-i and E. M. Landis, An algorithm for the organization of information, Soviet Mathematics?Doklady, vol.3, issue.5, pp.1259-1263, 1962.