C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi et al., CVC4, Computer Aided Verification, pp.171-177, 2011.
DOI : 10.1007/3-540-45657-0_40

C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB standard version 2.0, 2010.

N. Bjørner, Engineering theories with Z3. Programming Languages and Systems pp, pp.4-16, 2011.

F. Bobot, S. Conchon, E. Contejean, and S. Lescuyer, Implementing polymorphism in SMT solvers, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, SMT '08/BPR '08, pp.1-5, 2008.
DOI : 10.1145/1512464.1512466

S. Chatterjee, S. K. Lahiri, S. Qadeer, and Z. Rakamari´crakamari´c, 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

D. 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

C. Dross, J. C. Filliâtre, and Y. Moy, Correct Code Containing Containers, Proceedings of the 5th international conference on Tests and proofs, pp.102-118, 2011.
DOI : 10.1145/1375581.1375624
URL : https://hal.archives-ouvertes.fr/hal-00777683

Y. Ge, C. Barrett, and C. Tinelli, Solving quantified verification conditions using satisfiability modulo theories, LNCS, vol.4603, pp.21-167, 2007.
DOI : 10.1007/978-3-540-73595-3_12
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.192.6628

Y. Ge and L. De-moura, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification, pp.306-320, 2009.
DOI : 10.1007/978-3-642-02658-4_25

A. Goel, S. Krsti´ckrsti´c, and A. Fuchs, Deciding array formulas with frugal axiom instantiation, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, SMT '08/BPR '08, pp.12-17, 2008.
DOI : 10.1145/1512464.1512468

S. Jacobs and V. Kuncak, Towards Complete Reasoning about Axiomatic Specifications, Proceedings of VMCAI-12, pp.278-293, 2011.
DOI : 10.1007/978-3-540-25984-8_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.185.918

C. Lynch and B. Morawska, Automatic decidability, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.7-16, 2002.
DOI : 10.1109/LICS.2002.1029813
URL : https://hal.archives-ouvertes.fr/inria-00586936

C. Lynch, S. Ranise, C. Ringeissen, and D. K. Tran, Automatic decidability and combinability, Information and Computation, vol.209, issue.7, pp.1026-1047, 2011.
DOI : 10.1016/j.ic.2011.03.005
URL : https://hal.archives-ouvertes.fr/inria-00586936

S. Mcpeak and G. C. Necula, Data Structure Specifications via Local Equality Axioms, Computer Aided Verification, pp.476-490, 2005.
DOI : 10.1007/11513988_47

M. Moskal, Programming with triggers, Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT '09, pp.20-29, 2009.
DOI : 10.1145/1670412.1670416

L. De-moura and N. Bjørner, Efficient E-Matching for SMT Solvers, CADE-21, pp.183-198, 2007.
DOI : 10.1007/978-3-540-73595-3_13

L. De-moura and N. Bjørner, Engineering DPLL(T) + Saturation, IJCAR 2008, pp.475-490, 2008.
DOI : 10.1007/978-3-540-71070-7_40

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

G. Nelson, Techniques for program verification, 1981.

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006.
DOI : 10.1145/1217856.1217859

P. Rümmer, E-Matching with Free Variables, Logic for Programming, Artificial Intelligence , and Reasoning: 18th International Conference, LPAR-18, pp.359-374, 2012.
DOI : 10.1007/978-3-642-28717-6_28

P. Suter, R. Steiger, and V. Kuncak, Sets with Cardinality Constraints in Satisfiability Modulo Theories, Model Checking, and Abstract Interpretation, pp.403-418, 2011.
DOI : 10.1007/3-540-45988-X_9