S. Bardin, M. Delahaye, R. David, N. Kosmatov, M. Papadakis et al., Sound and Quasi-Complete Detection of Infeasible Test Requirements, 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST), pp.1-10, 2015.
DOI : 10.1109/ICST.2015.7102607

M. Barnett, B. E. Chang, R. Deline, B. Jacobs, and K. R. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, Proceedings of FMCO, number 4111 in LNCS, pp.364-387, 2005.
DOI : 10.1007/11804192_17
URL : http://research.microsoft.com/~leino/papers/krml160.pdf

M. Barnett and K. R. Leino, Weakest-precondition of unstructured programs, Proceedings of PASTE'05, pp.82-87, 2005.
DOI : 10.1145/1108768.1108813
URL : http://research.microsoft.com/~leino/papers/krml157.pdf

M. Barnett, K. R. Leino, and W. Schulte, The Spec# Programming System: An Overview, Proceedings of CASSIS, pp.49-69, 2004.
DOI : 10.1007/978-3-540-30569-9_3
URL : http://research.microsoft.com/~leino/papers/krml136.pdf

P. Baudin, J. C. Filliâtre, T. Hubert, C. Marché, B. Monate et al., ACSL: ANSI C Specification Language (preliminary design V1.2), preliminary edition, 2008.

S. Böhme and M. Moskal, Heaps and Data Structures: A Challenge for Automated Provers, Proceedigns of CADE-23, pp.177-191, 2011.
DOI : 10.1007/978-3-642-02959-2_10

D. Bühler, Structuring an Abstract Interpreter through Value and State Abstractions, 2017.

C. Calcagno, D. Distefano, P. O. Hearn, and H. Yang, Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic, SAS, pp.182-203, 2006.
DOI : 10.1007/11823230_13
URL : http://www.dcs.qmul.ac.uk/~ohearn/papers/beyond_reachability.pdf

B. Chang, X. Rival, and G. Necula, Shape Analysis with Structural Invariant Checkers, Proceedings of SAS, pp.384-401, 2007.
DOI : 10.1007/978-3-540-74061-2_24
URL : http://larsg.hautetfort.com/files/2007_228_007_RESU.pdf

S. Chatterjee, S. K. Lahiri, S. Qadeer, and Z. Rakamari?, A low-level memory model and an accompanying reachability predicate, International Journal on Software Tools for Technology Transfer, vol.20, issue.1, pp.105-116, 2009.
DOI : 10.1007/s10009-009-0098-1
URL : http://www.cs.ubc.ca/~zrakamar/publications/sttt2009-clqr.pdf

W. Chin, C. David, H. H. Nguyen, and S. Qin, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Science of Computer Programming, vol.77, issue.9, pp.1006-1036, 2012.
DOI : 10.1016/j.scico.2010.07.004
URL : https://doi.org/10.1016/j.scico.2010.07.004

L. Correnson, Qed. Computing What Remains to Be Proved, Proceedings of NFM, pp.215-229, 2014.
DOI : 10.1007/978-3-319-06200-6_17
URL : https://hal.archives-ouvertes.fr/cea-01809013

L. Correnson and F. Bobot, Exploring memory models with Frama-C/WP, 2017.

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/hal-01108790

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

C. Flanagan and J. B. Saxe, Avoiding exponential explosion, ACM SIGPLAN Notices, vol.36, issue.3, pp.193-205, 2001.
DOI : 10.1145/373243.360220

T. Hubert and C. Marché, Separation analysis for deductive verification, Proceedings of HAV, pp.81-93, 2007.

B. Jacobs and F. Piessens, The VeriFast program verifier, 2008.
DOI : 10.1007/978-3-642-17164-2_21
URL : https://lirias.kuleuven.be/bitstream/123456789/275140/1/aplas2010..

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-C: A software analysis perspective. Formal Asp, Comput, vol.27, issue.3, pp.573-609, 2015.
DOI : 10.1007/s00165-014-0326-7
URL : https://hal.archives-ouvertes.fr/cea-01808981

K. R. Leino, Efficient weakest preconditions, Information Processing Letters, vol.93, issue.6, pp.281-288, 2005.
DOI : 10.1016/j.ipl.2004.10.015
URL : http://research.microsoft.com/pubs/70052/tr-2004-34.pdf

X. Leroy, A. W. Appel, S. Blazy, and G. Stewart, The CompCert Memory Model, Version 2, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00703441

X. Leroy and S. Blazy, Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations, Journal of Automated Reasoning, vol.17, issue.5???6, pp.1-31, 2008.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/inria-00289542

F. Mehta and T. Nipkow, Proving pointer programs in higher-order logic, Proceedings of CADE-19, pp.121-135, 2003.
DOI : 10.1007/978-3-540-45085-6_10
URL : http://www4.in.tum.de/publ/papers/cade03.pdf

P. W. O-'hearn, J. C. Reynolds, and H. Yang, Local reasoning about programs that alter data structures, Proceedings of CSL, pp.1-19, 2001.

R. Piskac, T. Wies, and D. Zufferey, Automating Separation Logic with Trees and Data, Proceedings of CAV, pp.711-728, 2014.
DOI : 10.1007/978-3-319-08867-9_47

Z. Rakamaric and A. J. Hu, A Scalable Memory Model for Low-Level Code, Proceedings of VMCAI, pp.290-304, 2009.
DOI : 10.1145/1321631.1321719

P. Sotin, B. Jeannet, and X. , Concrete Memory Models for Shape Analysis, Electronic Notes in Theoretical Computer Science, vol.267, issue.1, pp.139-150, 2010.
DOI : 10.1016/j.entcs.2010.09.012
URL : https://hal.archives-ouvertes.fr/hal-00786330

W. Wang, C. Barrett, and T. Wies, Partitioned Memory Models for Program Analysis, Proceedings of VMCAI, pp.539-558, 2017.
DOI : 10.1145/301618.301647