]. M. Barnett, K. Leino, and W. Schulte, The Spec# Programming System: An Overview, CASSIS'04, pp.49-69, 2005.
DOI : 10.1007/978-3-540-30569-9_3

M. Barnett, B. Chang, R. Deline, B. Jacobs, and K. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, FMCO'05, pp.364-387, 2006.
DOI : 10.1007/11804192_17

M. Barnett, M. Fähndrich, and F. Logozzo, Embedded contract languages. SAC'10, 2010.

P. Chalin, J. Kinirya, G. Leavens, and E. Poll, Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2, FMCO'05, pp.77-101, 2006.
DOI : 10.1007/11804192_16

P. Cousot, Verification by abstract interpretation. Verification ? Theory & Practice, LNCS, vol.2772, pp.243-268, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00528611

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

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

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS'08, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

D. Dill, Timing assumptions and verification of finite-state concurrent systems Automatic Verification Methods for Finite State Systems, LNCS, vol.407, pp.197-212, 1989.

I. Dillig, T. Dillig, and A. Aiken, Fluid Updates: Beyond Strong vs. Weak Updates, LNCS, vol.10, issue.6012, pp.246-266, 2010.
DOI : 10.1007/978-3-642-11957-6_14

I. Dillig, T. Dillig, and A. Aiken, Precise reasoning for programs using containers, 2011.

M. Fähndrich and F. Logozzo, Static contract checking with abstract interpretation. FoVeOOS'10, LNCS, 2010.

C. Flanagan and S. Qadeer, Predicate abstraction for software verification, 29th POPL, pp.191-202, 2002.

G. Int, Garmin device interface specification, Garmin Int., Inc

D. Gopan, T. Reps, and S. Sagiv, A framework for numeric analysis of array operations, pp.338-350, 2005.

S. Gulwani, B. Mccloskey, and A. Tiwari, Lifting abstract interpreters to quantified logical domains, 35th POPL, pp.235-246, 2008.

N. Halbwachs and M. Péron, Discovering properties about arrays in simple programs, pp.339-348, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00288274

R. Jhala and K. Mcmillan, Array Abstractions from Proofs, CAV'07, pp.193-206, 2007.
DOI : 10.1007/978-3-540-73368-3_23

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

L. Kovács and A. Voronkov, Finding loop invariants for programs over arrays using a theorem prover, LNCS, vol.5503, pp.470-485, 2009.

V. Laviron and F. Logozzo, SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities, LNCS, vol.5403, pp.229-244, 2009.
DOI : 10.1007/978-3-540-93900-9_20

S. Lee and D. Cho, Packet-scheduling algorithm based on priority of separate buffers for unicast and multicast services, Electronics Letters, vol.39, issue.2, pp.259-260, 2003.
DOI : 10.1049/el:20030157

F. Logozzo, Class-Level Modular Analysis for Object Oriented Languages, SAS'03, pp.37-54, 2003.
DOI : 10.1007/3-540-44898-5_3

F. Logozzo and M. Fähndrich, On the Relative Completeness of Bytecode Analysis Versus Source Code Analysis, CC'08, pp.197-212, 2008.
DOI : 10.1007/978-3-540-78791-4_14

F. Logozzo and M. Fähndrich, Pentagons, Proceedings of the 2008 ACM symposium on Applied computing , SAC '08, pp.184-188, 2008.
DOI : 10.1145/1363686.1363736

M. Marron, D. Stefanovic, M. Hermenegildo, and D. Kapur, Heap analysis in the presence of collection libraries. PASTE'07, pp.31-36, 2007.

K. L. Mcmillan, Quantified Invariant Generation Using an Interpolating Saturation Prover, TACAS'08, pp.197-212, 2008.
DOI : 10.1007/978-3-540-78800-3_31

B. Meyer, Eiffel: The Language, 1991.

A. Miné, The octagon abstract domain. Higher-Order and Symbolic Computation, pp.31-100, 2006.

V. Pratt, Two easy theories whose combination is hard

B. Roy, Transitivité et connexité Comptes-Rendus de l'Académie des Sciences de Paris, Sér. A-B, vol.249, pp.216-218, 1959.

M. Seghir, A. Podelski, and T. Wies, Abstraction Refinement for Quantified Array Assertions, SAS'09, pp.3-18, 2009.
DOI : 10.1007/11547662_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.211.9930

R. Shostak, Deciding Linear Inequalities by Computing Loop Residues, Journal of the ACM, vol.28, issue.4, pp.769-779, 1981.
DOI : 10.1145/322276.322288
URL : http://www.dtic.mil/get-tr-doc/pdf?AD=ADA055868

H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook et al., Scalable Shape Analysis for Systems Code, CAV'98, pp.385-398, 2008.
DOI : 10.1007/978-3-540-70545-1_36