L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.217-247, 1994.
DOI : 10.1093/logcom/4.3.217

K. Bansal, A. Reynolds, T. King, C. W. Barrett, and T. Wies, Deciding Local Theory Extensions via E-matching, Computer Aided Verification -27th International Conference, CAV 2015 Proceedings, Part II, pp.87-105, 2015.
DOI : 10.1007/978-3-319-21668-3_6
URL : http://arxiv.org/pdf/1508.06827

H. Barbosa, Efficient instantiation techniques in SMT (work in progress), Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning, pp.1-10, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01388976

C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB Standard: Version 2.0, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, 2010.

C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, Satisfiability modulo theories, Handbook of Satisfiability, pp.825-885, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01095009

A. Biere, Bounded Model Checking, Handbook of Satisfiability, pp.457-481, 2009.
DOI : 10.1016/S0065-2458(03)58003-2

A. R. Bradley, Z. Manna, and H. B. Sipma, What's Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation, 7th International Conference Proceedings, pp.427-442, 2006.

A. Brillout, D. Kroening, P. Rümmer, and T. Wahl, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, Verification, Model Checking, and Abstract Interpretation -12th International Conference, VMCAI 2011. Proceedings, pp.88-102, 2011.
DOI : 10.1007/978-3-642-11319-2_12

R. Brummayer and A. Biere, Boolector: An efficient SMT solver for bit-vectors and arrays. In Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software. Proceedings, pp.174-177, 2009.

R. David, S. Bardin, T. D. Ta, L. Mounier, J. Feist et al., BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis, 2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER), pp.653-656, 2016.
DOI : 10.1109/SANER.2016.43

L. M. De-moura and N. Bjørner, Z3: an efficient SMT solver In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference , TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software. Proceedings, pp.337-340, 2008.

D. E. Denning and P. J. Denning, Certification of programs for secure information flow, Communications of the ACM, vol.20, issue.7, pp.504-513, 1977.
DOI : 10.1145/359636.359712

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, S. Conchon, J. Kanig, and A. Paskevich, Reasoning with triggers, 10th International Workshop on Satisfiability Modulo Theories, SMT 2012, pp.22-31, 2012.
DOI : 10.29007/3c1n
URL : https://hal.archives-ouvertes.fr/hal-00703207

C. Dross, S. Conchon, J. Kanig, and A. Paskevich, Adding Decision Procedures to SMT Solvers Using Axioms with Triggers, Journal of Automated Reasoning, vol.53, issue.6, pp.387-457, 2016.
DOI : 10.1007/978-3-642-18275-4_28
URL : https://hal.archives-ouvertes.fr/hal-00915931

Y. Ge and L. M. De-moura, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification, 21st International Conference Proceedings, pp.306-320, 2009.
DOI : 10.1007/978-3-540-78800-3_19

P. Godefroid, M. Y. Levin, and D. A. Molnar, SAGE, Communications of the ACM, vol.55, issue.3, p.20, 2012.
DOI : 10.1145/2093548.2093564

C. Ihlemann, S. Jacobs, and V. Sofronie-stokkermans, On Local Reasoning in Verification In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference. Proceedings, pp.265-281, 2008.

L. Kovács and A. Voronkov, First-Order Theorem Proving and Vampire, Computer Aided Verification -25th International Conference, CAV 2013 Proceedings, pp.1-35, 2013.
DOI : 10.1007/978-3-642-39799-8_1

D. Kroening and O. Strichman, Decision Procedures -An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, 2008.

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, Handbook of Automated Reasoning (in 2 volumes), pp.371-443, 2001.
DOI : 10.1016/B978-044450813-3/50009-6
URL : http://www-lsi.upc.es/~albert/papers/handbook.ps.gz

P. Ørbaek, Can you trust your data? In TAPSOFT'95: Theory and Practice of Software Development, 6th International Joint Conference CAAP/FASE Proceedings, pp.575-589, 1995.

A. Reynolds, M. Deters, V. Kuncak, C. Tinelli, and C. W. Barrett, Counterexample-Guided Quantifier Instantiation for Synthesis in SMT, Computer Aided Verification -27th International Conference, CAV 2015 Proceedings, Part II, pp.198-216, 2015.
DOI : 10.1007/978-3-319-21668-3_12

A. Reynolds, C. Tinelli, and L. M. De-moura, Finding conflicting instances of quantified formulas in SMT, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.195-202, 2014.
DOI : 10.1109/FMCAD.2014.6987613

A. Reynolds, C. Tinelli, A. Goel, and S. Krstic, Finite Model Finding in SMT, Computer Aided Verification -25th International Conference, CAV 2013 Proceedings, pp.640-655, 2013.
DOI : 10.1007/978-3-642-39799-8_42

A. Reynolds, C. Tinelli, A. Goel, S. Krstic, M. Deters et al., Quantifier Instantiation Techniques for Finite Model Finding in SMT, Automated Deduction -CADE-24 -24th International Conference on Automated Deduction, Lake Placid. Proceedings, pp.377-391, 2013.
DOI : 10.1007/978-3-642-38574-2_26

A. Riazanov and A. Voronkov, The design and implementation of VAMPIRE, pp.91-110, 2002.

S. Schulz, E -a brainiac theorem prover, AI Commun, vol.15, issue.2-3, pp.111-126, 2002.

G. Smith, Principles of Secure Information Flow Analysis, Malware Detection, pp.291-307, 2007.
DOI : 10.1007/978-0-387-44599-1_13

C. M. Wintersteiger, Y. Hamadi, and L. M. De-moura, Efficiently solving quantified bit-vector formulas, Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, pp.239-246, 2010.
DOI : 10.1016/0022-0000(80)90027-6
URL : http://research.microsoft.com/%7Eleonardo/fmcad10.pdf