. Barnett, R. Bor-yuh-evan-chang, K. Deline, M. Rustan, and . Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, FMCO, pp.364-387, 2005.
DOI : 10.1007/11804192_17

J. Patrick-baudin, C. Filliâtre, B. Marché, Y. Monate, V. Moy et al., ACSL: ANSI/ISO C Specification Language, 2008.

[. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, PLDI 2001, pp.203-213, 2001.

R. Bornat, Proving Pointer Programs in Hoare Logic, Mathematics of Program Construction, pp.102-126, 2000.
DOI : 10.1007/10722010_8

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986.
DOI : 10.1109/TC.1986.1676819

A. Cimatti, A. Franzen, A. Griggio, K. Kalyanasundaram, and M. Roveri, Tighter integration of BDDs and SMT for Predicate Abstraction, 2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010), 2010.
DOI : 10.1109/DATE.2010.5457090
URL : https://hal.archives-ouvertes.fr/inria-00535785

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM, pp.752-794, 2003.
DOI : 10.1145/876638.876643

W. Craig, Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, The Journal of Symbolic Logic, vol.14, issue.03, pp.269-285, 1957.
DOI : 10.2307/2963594

A. Michael, S. Colón, H. B. Sankaranarayanan, and . Sipma, Linear invariant generation using non-linear constraint solving, Proceedings of Computer Aided Verification, CAV 2003, pp.420-432, 2003.

[. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.
DOI : 10.1145/1066100.1066102

K. Cormac-flanagan, M. Rustan, M. Leino, G. Lillibridge, J. B. Nelson et al., Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, PLDI '02, pp.234-245, 2002.

J. Filliâtre and C. Marché, Multi-prover Verification of C Programs, ICFEM, pp.15-29, 2004.
DOI : 10.1007/978-3-540-30482-1_10

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

C. Flanagan and S. Qadeer, Predicate abstraction for software verification, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL 2002, pp.191-202, 2002.

S. Bhargav, S. Gulavani, A. V. Chakraborty, S. K. Nori, and . Rajamani, Automatically Refining Abstract Interpretations In Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems, TACAS'08/ETAPS'08, pp.443-458, 2008.

A. Gupta and A. Rybalchenko, InvGen: An Efficient Invariant Generator, CAV, pp.634-640, 2009.
DOI : 10.1007/978-3-642-02658-4_48
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.164.7483

S. Graf and H. Saïdi, Construction of abstract state graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, pp.72-83, 1997.
DOI : 10.1007/3-540-63166-6_10

S. Gulwani, . Srivastava, . Saurabh, and R. Venkatesan, Constraint-Based Invariant Inference over Predicate Abstraction, Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI '09, pp.120-135, 2009.
DOI : 10.1007/978-3-540-93900-9_13
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.147.8895

T. Hubert, Analyse Statique et preuve de Programmes Industriels Critiques, Thèse de doctorat, 2008.

]. K. Kal09 and . Kalyanasundaram, CEGAR Using SMT Solvers for Predicate Abstraction, 2009.

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

M. Colón, S. Sankaranarayanan, and H. Sipma, Linear Invariant Generation Using Non-linear Constraint Solving, CAV, pp.420-432, 2003.
DOI : 10.1007/978-3-540-45069-6_39

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff, Proceedings of the 38th conference on Design automation , DAC '01, pp.530-535, 2001.
DOI : 10.1145/378239.379017

Y. Moy, Automatic Modular Static Safety Checking for C Programs, 2009.

R. Sharma, I. Dillig, T. Dillig, and A. Aiken, Simplifying Loop Invariant Generation Using Splitter Predicates, CAV, page To Appear, 2011.
DOI : 10.1007/s10990-006-8609-1

[. Srivastava and S. Gulwani, Program verification using templates over predicate abstraction, Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation, PLDI 2009, pp.223-234, 2009.
DOI : 10.1145/1543135.1542501
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.148.403

H. Peter, B. Schmitt, and . Weiß, Inferring invariants by symbolic execution

B. Weiß, Predicate abstraction in a program logic calculus, Science of Computer Programming, 2011.