J. Guitton, J. Kanig, and Y. Moy, Why Hi-Lite Ada?, Boogie, pp.27-39, 2011.

M. Barnett, R. Deline, B. Jacobs, B. Y. Chang, and K. R. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, In: FMCO. LNCS, vol.4111, 2005.
DOI : 10.1007/11804192_17

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

F. Bobot and A. Paskevich, Expressing Polymorphic Types in a Many-Sorted Language, In: FroCoS. LNCS, vol.40, issue.1, pp.87-102, 2011.
DOI : 10.1007/978-3-540-78800-3_24
URL : https://hal.archives-ouvertes.fr/inria-00591414

D. E. Knuth, J. H. Morris, and V. R. Pratt, Fast Pattern Matching in Strings, SIAM Journal on Computing, vol.6, issue.2, pp.323-350, 1977.
DOI : 10.1137/0206024

K. R. Leino and M. Moskal, VACID-0: Verification of ample correctness of invariants of data-structures, edition 0, 2010.