F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-C: A software analysis perspective, Formal Aspects of Computing, pp.573-609, 2015.
URL : https://hal.archives-ouvertes.fr/cea-01808981

P. Baudin, P. Cuoq, J. Filiâtre, C. Marché, B. Monate et al., ACSL: ANSI/ISO C Specification Language

V. Robles, N. Kosmatov, V. Prevosto, L. Rilling, and P. L. Gall, MetAcsl: Specification and Verification of High-Level Properties, Tools and Algorithms for the Construction and Analysis of Systems, pp.358-364, 2019.
URL : https://hal.archives-ouvertes.fr/cea-02019790

P. Baudin, F. Bobot, L. Correnson, and Z. Dargaye, WP plugin manual

J. Signoles, N. Kosmatov, and K. Vorobyov, E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper), International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, pp.164-173, 2017.

G. Petiot, N. Kosmatov, B. Botella, A. Giorgetti, and J. Julliand, How testing helps to diagnose proof failures, Formal Aspects of Computing, pp.629-657, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01948799

G. T. Leavens, A. L. Baker, and C. Ruby, JML: A Notation for Detailed Design, Behavioral Specifications of Businesses and Systems, pp.175-188, 1999.

Y. Cheon and A. Perumandla, Specifying and Checking Method Call Sequences in JML, International Conference on Software Engineering Research and Practice, pp.511-516, 2005.

K. Trentelman and M. Huisman, Extending JML Specifications with Temporal Logic, International Conference on Algebraic Methodology and Software Technology. AMAST, pp.334-348, 2002.

N. Stouls and J. Groslambert, Vérification de propriétés LTL sur des programmes C par génération d'annotations, 2011.

S. Oliveira, V. Prevosto, and S. Bensalem, CaFE: a model-checker collaboratif, Approches Formelles dans l'Assistance au Developpement Logiciel, 2017.

L. Blatter, N. Kosmatov, P. L. Gall, V. Prevosto, and G. Petiot, Static and Dynamic Verification of Relational Properties on Self-composed C Code, International Conference on Tests and Proofs, 2018.
URL : https://hal.archives-ouvertes.fr/cea-01835470

M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J. Lanet, Enforcing High-Level Security Properties for Applets, International Conference on Smart Card Research and Advanced Applications, pp.1-16, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00071523

G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. V. Lopes et al., Aspect-Oriented Programming, European Conference on Object-Oriented Programming, pp.220-242, 1997.