A. Aiken, J. S. Foster, J. Kodumal, and T. Terauchi, Checking and inferring local non-aliasing, PLDI '03: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pp.129-140, 2003.

M. G. Assaad and G. T. Leavens, Alias-free parameters in C for better reasoning and optimization, 2001.

M. Barnett, K. R. Leino, and W. Schulte, The Spec# Programming System: An Overview, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. CASSIS'04, pp.49-69, 2004.
DOI : 10.1007/978-3-540-30569-9_3

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

F. Bourdoncle, Assertion-based debugging of imperative programs by abstract interpretation, ESEC '93: Proceedings of the 4th European Software Engineering Conference on Software Engineering, pp.501-516, 1993.
DOI : 10.1007/3-540-57209-0_33

A. R. Bradley and Z. Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, 2007.

C. Calcagno, D. Distefano, P. W. O-'hearn, and H. Yang, Footprint Analysis: A Shape Analysis That Discovers Preconditions, Proceedings of the 14th International Static Analysis Symposium, pp.402-418, 2007.
DOI : 10.1007/978-3-540-74061-2_25

S. Chaki and S. Hissam, Certifying the absence of buffer overflows, 2006.

M. Colon, S. Sankaranarayanan, and H. Sipma, Linear Invariant Generation Using Non-linear Constraint Solving, Proc. of the Int. Conf. on Computer Aided Verification, CAV. In: Lecture Notes in Computer Science, pp.420-432, 2003.
DOI : 10.1007/978-3-540-45069-6_39

S. Conchon and E. Contejean, The Alt-Ergo automatic theorem prover http, 2008.

J. Couchot and T. Hubert, A Graph-based Strategy for the Selection of Hypotheses, FTP 2007 ? International Workshop on First-Order Theorem Proving, 2007.

P. Cousot and R. Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '79, pp.269-282, 1979.
DOI : 10.1145/567752.567778

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, pp.84-96, 1978.
DOI : 10.1145/512760.512770

M. Dahlweid, M. Moskal, T. Santen, S. Tobies, and W. Schulte, VCC: Contract-based modular verification of concurrent C, 2009 31st International Conference on Software Engineering, Companion Volume, pp.429-430, 2009.
DOI : 10.1109/ICSE-COMPANION.2009.5071046

E. W. Dijkstra, A Discipline of Programming, Series in Automatic Computation, 1976.

D. L. Dill, Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits, 1989.

J. Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of functional Programming, vol.13, issue.4, pp.709-745, 2003.
DOI : 10.1017/S095679680200446X

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, 19th International Conference on Computer Aided Verification, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

C. Flanagan, K. R. Leino, . Esc, and . Java, Houdini, an annotation assistant for, FME'01: Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, pp.500-517, 2001.

S. Gulwani and A. Tiwari, Combining abstract interpreters, Annual ACM Conference on Programming Language Design and Implementation, 2006.

S. Gulwani and A. Tiwari, Assertion Checking Unified, The 8th International Conference on Verification, Model Checking and Abstract Interpretation, pp.363-377, 2007.
DOI : 10.1007/978-3-540-69738-1_26

B. Hackett, M. Das, D. Wang, and Z. Yang, Modular checking for buffer overflows in the large, Proceeding of the 28th international conference on Software engineering , ICSE '06, pp.232-241, 2006.
DOI : 10.1145/1134285.1134319

T. E. Hart, K. Ku, D. Lie, M. Chechik, and A. Gurfinkel, PtYasm: Software Model Checking with Proof Templates, 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, 2008.
DOI : 10.1109/ASE.2008.80

J. Hatcliff, G. T. Leavens, K. R. Leino, P. Miller, and M. Parkinson, Behavioral interface specification languages, ACM Computing Surveys, vol.44, issue.3, 2009.
DOI : 10.1145/2187671.2187678

T. Hubert and C. Marché, Separation analysis for deductive verification In: Heap Analysis and Verification, HAV'07, pp.81-93, 2007.

M. Janota, Assertion-based loop invariant generation, Proceedings of the 1st International Workshop on Invariant Generation, WING'07. Hagenberg, Austria, workshop at CALCULEMUS, 2007.

T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney et al., Cyclone: A safe dialect of C, Proc. 2002 USENIX Annual Technical Conference, pp.275-288, 2002.

M. Karr, Affine relationships among variables of a program, Acta Informatica, vol.6, issue.2, pp.133-151, 1976.
DOI : 10.1007/BF00268497

B. W. Kernighan and D. M. Ritchie, The C Programming Language, 1978.

D. Koes, M. Budiu, and G. Venkataramani, Programmer specified pointer independence, Proceedings of the 2004 workshop on Memory system performance , MSP '04, pp.51-59, 2004.
DOI : 10.1145/1065895.1065905

K. Ku, T. E. Hart, M. Chechik, and D. Lie, A buffer overflow benchmark for software model checkers, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering , ASE '07, pp.389-392, 2007.
DOI : 10.1145/1321631.1321691

C. Lattner, A. Lenharth, and V. Adve, Making context-sensitive points-to analysis with heap cloning practical for the real world, ACM SIGPLAN Notices, vol.42, issue.6, pp.278-289, 2007.
DOI : 10.1145/1273442.1250766

K. R. Leino and F. Logozzo, Loop Invariants on Demand, APLAS'05: Proceedings of The 3rd ASIAN Symposium on Programming Languages and Systems. In: LNCS, pp.119-134, 2005.
DOI : 10.1007/11575467_9

K. R. Leino and F. Logozzo, Using widenings to infer loop invariants inside an SMT solver, or: a theorem prover as abstract domain, p.7, 2007.

K. R. Leino, J. B. Saxe, and R. Stata, Checking Java programs via guarded commands, Proceedings of the Workshop on Object-Oriented Technology, pp.110-111, 1999.

D. Liang and M. J. Harrold, Efficient Computation of Parameterized Pointer Information for Interprocedural Analyses, SAS'01: Proceedings of the 8th International Symposium on Static Analysis, pp.279-298, 2001.
DOI : 10.1007/3-540-47764-0_16

C. Marché, Jessie, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.1-2, 2007.
DOI : 10.1145/1292597.1292598

A. Miné, The octagon abstract domain, Higher-Order and Symbolic Computation, vol.2477, issue.3, pp.31-100, 2006.
DOI : 10.1007/s10990-006-8609-1

D. Monniaux, A Quantifier Elimination Algorithm for Linear Real Arithmetic, 2008.
DOI : 10.1007/978-3-540-89439-1_18
URL : https://hal.archives-ouvertes.fr/hal-00262312

Y. Moy, Automatic modular static safety checking for C programs, 2009.

M. Norrish, C formalised in HOL, 1998.

C. Popeea, D. N. Xu, and W. Chin, A practical and precise inference and specializer for array bound checks elimination, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation , PEPM '08, pp.177-187, 2008.
DOI : 10.1145/1328408.1328434

J. C. Reynolds, Syntactic control of interference, POPL'78: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp.39-46, 1978.

X. Rival, Understanding the Origin of Alarms in Astr??e, 12th Static Analysis Symposium. SAS'05. In: LNCS, pp.303-319, 2005.
DOI : 10.1007/11547662_21

N. Rousset, Automatisation de la spécification et de la vérification d'applications Java Card, Thèse de doctorat, 2008.

A. Starostin, Formal verification of a C-library for strings, 2006.

B. Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.32-41, 1996.
DOI : 10.1145/237721.237727

N. Suzuki and K. Ishihata, Implementation of an array bound checker, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.132-143, 1977.
DOI : 10.1145/512950.512963

J. Talpin and P. Jouvelot, Abstract, Journal of Functional Programming, vol.78, issue.03, 1991.
DOI : 10.1145/322123.322135
URL : https://hal.archives-ouvertes.fr/hal-00730926

J. Talpin and P. Jouvelot, The type and effect discipline, Seventh Annual IEEE Symposium on Logic in Computer Science, pp.162-173, 1992.

M. Tofte and J. Talpin, Region-Based Memory Management, Information and Computation, vol.132, issue.2, 1997.
DOI : 10.1006/inco.1996.2613

V. Weispfenning, Complexity and uniformity of elimination in Presburger arithmetic, Proceedings of the 1997 international symposium on Symbolic and algebraic computation , ISSAC '97, pp.48-53, 1997.
DOI : 10.1145/258726.258746

Z. Xu, Safety checking of machine code, 2000.

Z. Xu, B. P. Miller, and T. Reps, Safety checking of machine code, ACM SIGPLAN Notices, vol.35, issue.5, pp.70-82, 2000.
DOI : 10.1145/358438.349313

M. Zitser, R. Lippmann, and T. Leek, Testing static analysis tools using exploitable buffer overflows from open source code, ACM SIGSOFT Software Engineering Notes, vol.29, issue.6, pp.97-106, 2004.
DOI : 10.1145/1041685.1029911