P. Baudin, J. Filliâtre, C. Marché, B. Monate, Y. Moy et al., ACSL : ANSI/ISO C specification language, 2008.

F. Bobot, J. 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. 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. Filliâtre, L. Gondelman, and A. Paskevich, A pragmatic type system for deductive verification, Research report, 2016.

J. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code. Formal Methods in System Design, pp.152-174, 2016.

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

K. Rustan, M. Leino, and M. Moskal, Usable auto-active verification, Usable Verification Workshop, 2010.

R. Rieu-helft, C. Marché, and G. Melquiond, How to Get an Efficient yet Verified Arbitrary-Precision Integer Library, 9th Working Conference on Verified Software : Theories, Tools, and Experiments, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01519732