]. R. Références1, M. Alur, K. Benedikt, P. Etessami, T. Godefroid et al., Analysis of recursive state machines, ACM TOPLAS, vol.27, issue.4, 2005.

R. Alur, K. Etessami, and P. Madhusudan, A Temporal Logic of Nested Calls and Returns, Tools and Algorithms for the Construction and Analysis of Systems, pp.467-481, 2004.
DOI : 10.1007/978-3-540-24730-2_35

T. Ball, V. Levin, and S. K. Rajamani, A decade of software model checking with SLAM, Communications of the ACM, vol.54, issue.7, pp.68-76, 2011.
DOI : 10.1145/1965724.1965743

T. Ball and S. K. Rajamani, Slic : a Specification Language for Interface Checking (of C) Microsoft Research, 2002.

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

M. Benedikt, P. Godefroid, and T. Reps, Model Checking of Unrestricted Hierarchical State Machines, Automata, Languages and Programming, pp.652-666, 2001.
DOI : 10.1007/3-540-48224-5_54

D. Beyer and M. E. Keremoglu, CPAchecker: A Tool for Configurable Software Verification, Proceedings of CAV (Computer Aided Verification), pp.184-190, 2011.
DOI : 10.1007/978-3-540-31980-1_40

G. Canet, P. Cuoq, and B. Monate, A Value Analysis for C Programs, 2009 Ninth IEEE International Working Conference on Source Code Analysis and Manipulation, 2009.
DOI : 10.1109/SCAM.2009.22

E. Clarke, K. Mcmillan, S. Campos, and V. Hartonas-garmhausen, Symbolic model checking, Computer Aided Verification, pp.419-422, 1996.
DOI : 10.1007/3-540-61474-5_93

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, International Conference on Software Engineering and Formal Methods (SEFM'12, 2012.
DOI : 10.1007/978-3-642-33826-7_16

J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon, Efficient Algorithms for Model Checking Pushdown Systems, Computer Aided Verification, pp.232-247, 2000.
DOI : 10.1007/10722167_20

P. Gastin and D. Oddoux, Fast ltl to büchi automata translation, Computer Aided Verification, pp.53-65, 2001.

A. Giorgetti, J. Groslambert, J. Julliand, and O. Kouchnarenko, Verification of class liveness properties with Java modelling language, IET Software, vol.2, issue.6, pp.500-514, 2008.
DOI : 10.1049/iet-sen:20080008

G. J. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, 1997.
DOI : 10.1109/32.588521

R. Jhala and R. Majumdar, Software model checking, ACM Computing Surveys, vol.41, issue.4, 2009.
DOI : 10.1145/1592434.1592438

F. Merz, S. Falke, and C. Sinz, LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR, VSTTE, 2012.
DOI : 10.1007/978-3-540-93900-9_24

B. Meyer, Applying 'design by contract', Computer, vol.25, issue.10, 1992.
DOI : 10.1109/2.161279

G. C. Necula, S. Mcpeak, S. P. Rahul, and W. Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Compiler Construction, 2002.
DOI : 10.1007/3-540-45937-5_16

F. Nielson, H. R. Nielson, and C. Hankin, Principles of program analysis, 1999.
DOI : 10.1007/978-3-662-03811-6

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-77, 1977.
DOI : 10.1109/SFCS.1977.32

A. N. Prior, Time and modality, 1957.

N. Stouls and V. Prevosto, Aoraï plug-in tutorial, version Nitrogen, 2011.