, teurs, tableaux, bit-vecteurs, datatypes, symboles non interprétés et arithmétique sur les entiers et rationnels. Pour résoudre cette dernière, il faut donc à la fois gérer de nombreuses théories

, Ces tests sont principalement fournis par des acteurs de la communauté SMT. Toute personne peut proposer des problèmes au format de la SMT-LIB 2. Ces problèmes, s'ils sont conformes à la SMT-LIB 2, sont triés selon les logiques nécessaires pour leur résolution, puis ajoutés à l'ensemble des bancs de test. Ces problèmes sont dits non incrémentaux lorsqu'ils ne possèdent qu'une commande check-sat, sinon ils sont catégorisés en incrémental s'ils alternent assertions et commande check-sat. Il peut exister différents types de problèmes. Les crafted sont des fichiers créés à la main ou générés automatiquement et ayant pour but de vérifier un problème complexe ou une nouveauté de la SMT-LIB 2. Les problèmes random sont des problèmes auto-génerés aléatoirement, et les problèmes industrial sont issus du monde industriel. La quantité de fichiers de tests de la SMT-LIB 2 s'élève aujourd'hui à plus de 300 000, répartis en 51 logiques différentes. La communauté SMT dispose aussi d'un accès au cluster Starexec 2 , financé par la National Science Foundation. Cette plate-forme utilisée pour la résolution de problèmes est partagée avec d'autres communautés comme TPTP, Bancs de tests de la communauté SMT La communauté SMT a à sa disposition plusieurs outils permettant son bon développement. Elle dispose en effet d'un ensemble important de bancs de test, disponibles à tous

, Règles de la compétition Nous allons présenter succinctement les règles de la compétition SMT-COMP 2018 (voir ici pour plus de détails, vol.4

, Chaque membre de la communauté SMT peut soumettre son solveur à la compétition en spécifiant les catégories dans lesquelles il souhaite participer, vol.1

, Globalement Alt-Ergo a été aussi performant que l'an passé, bien que nous ne soyons pas très efficaces sur les problèmes sans quantificateur. Cela nous montre qu'encore beaucoup d'efforts restent à produire concernant nos théories, p.136

, Chapitre 6. Participation à la compétition SMT-COMP

F. Logic, , pp.35-68, 2007.

L. Bachmair, A. Tiwari, and L. Vigneron, Abstract congruence closure, Journal of Automated Reasoning, vol.31, issue.2, pp.129-168, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099511

C. Barett, P. Fontaine, and C. Tinelli, Smt-lib 3 : Bringing higher-order logic to smt, 2018.

C. Barrett and J. Donham, Combining sat methods with non-clausal decision heuristics, Electron. Notes Theor. Comput. Sci, vol.125, issue.3, pp.3-12, 2005.

C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB Standard : Version 2.5, 2015.

C. Barrett, P. Fontaine, and C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB), 2016.

C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB Standard : Version 2.6, 2017.

C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB Standard : Version 2.0, 2010.

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

C. Barrett and C. Tinelli, CVC4 : the SMT solver

A. Biere, A. Biere, M. Heule, H. Van-maaren, and T. Walsh, Handbook of Satisfiability : Volume 185 Frontiers in Artificial Intelligence and Ap-Bibliographie plications, 2009.

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

F. Bobot and A. Paskevich, Expressing Polymorphic Types in a Many-Sorted Language, pp.87-102
URL : https://hal.archives-ouvertes.fr/inria-00591414

F. Bobot, J. Filliâtre, C. Marché, G. Melquiond, and A. Paskevich, Preserving User Proofs Across Specification Changes, Fifth Working Conference on Verified Software : Theories, Tools and Experiments, vol.8164, pp.191-201, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00875395

-. Hans and . Boehm, Reducing garbage collector cache misses, 2000.

R. Bonichon, D. Déharbe, and C. Tavares, Extending SMT-LIB v2 with ?-terms and polymorphism, Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, SMT 2014, vol.1163, pp.53-62, 2014.

Ç. Bozman, Memory profiling of OCaml applications. Theses, ENSTA ParisTech, 2014.
URL : https://hal.archives-ouvertes.fr/tel-01122262

Ç. Bozman, G. Henry, M. Iguernelala, F. L. Fessant, and M. Mauny, ocp-memprof : un profileur mémoire pour OCaml, Vingt-sixièmes Journées Francophones des Langages Applicatifs, 2015.

C. J. Cheney, A nonrecursive list compacting algorithm, Commun. ACM, vol.13, issue.11, pp.677-678, 1970.

F. Jean-christophe and S. Conchon, Type-safe modular hashconsing, In : Proceedings of the 2006 workshop on ML, pp.12-19, 2006.

E. Sylvain-conchon, M. Contejean, and . Iguernelala, Canonized rewriting and ground AC completion modulo shostak theories : Design and implementation, Logical Methods in Computer Science, vol.8, issue.3, 2012.

E. Sylvain-conchon, J. Contejean, S. Kanig, and . Lescuyer, Cc(x) : Semantic combination of congruence closure with solvable theories, Electronic Notes in Theoretical Computer Science, vol.198, issue.2, pp.51-69, 2008.

A. Sylvain-conchon and . Coquereau, Mohamed Iguernelala, and Alain Mebsout, Proceedings of the 16th International Workshop on Satisfiability Modulo Theories, SMT 2018, 2018.

M. Sylvain-conchon, K. Iguernlala, G. Ji, C. Melquiond, and . Fumex, A three-tier strategy for reasoning about floating-point numbers in smt, Computer Aided Verification, pp.419-435, 2017.

M. Sylvain-conchon, A. Iguernlala, and . Mebsout, AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo, Proceedings of the 12th Workshop on User Interfaces for Theorem Provers, pp.1-13, 2016.

J. Couchot and S. Lescuyer, Handling polymorphism in automated deduction, 21th International Conference on Automated Deduction (CADE-21), vol.4603, pp.263-278, 2007.

S. Cruanes, Faithful reimplementation of minisat 2.2 in ocaml, 2018.

G. B. Dantzig, Linear Programming and Extensions, 1991.

M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Commun. ACM, vol.5, issue.7, pp.394-397, 1962.

M. Davis and H. Putnam, A computing procedure for quantification theory, J. ACM, vol.7, issue.3, pp.201-215, 1960.

L. De-moura and N. Bjørner, Z3, an efficient SMT solver

L. De-moura and N. Bjorner, Relevancy propagation, 2007.

D. Déharbe, P. Fontaine, D. L. Berre, and B. Mazure, Computing prime implicants, pp.46-52, 2013.

D. Delahaye, C. Dubois, C. Marché, D. Mentré, ;. Tla et al., The bware project : Building a proof platform for the automated verification of b proof obligations, Abstract State Machines, pp.290-293, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00998092

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify : A theorem prover for program checking, J. ACM, vol.52, issue.3, pp.365-473, 2005.

D. Doligez and G. Gonthier, Portable, unobtrusive garbage collection for multiprocessor systems, Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '94, pp.70-83, 1994.

D. Doligez and X. Leroy, A concurrent, generational garbage collector for a multithreaded implementation of ML, POPL 1993 : 20th symposium Principles of Programming Languages, pp.113-123, 1993.
URL : https://hal.archives-ouvertes.fr/hal-01499969

D. Déharbe and P. Fontaine, The veriT SMT solver

N. Eén and N. Sörensson, An extensible sat-solver, Theory and Applications of Satisfiability Testing, pp.502-518, 2004.

U. Egly and L. Haller, A sat solver for circuits based on the tableau method, vol.24, pp.15-23, 2010.

J. Filliâtre, One Logic To Use Them All, CADE 24 -the 24th International Conference on Automated Deduction, 2013.

J. , C. Filliâtre, and A. Paskevich, Why3 -where programs meet provers, Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems, pp.125-128, 2013.

J. , C. Filliâtre, and A. Paskevich, Why3 -Where Programs Meet Provers, ESOP'13 22nd European Symposium on Programming, vol.7792, 2013.

H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Dpll(t) : Fast decision procedures, vol.06, 2004.

L. Hadarean, K. Bansal, D. Jovanovi?, C. Barrett, and C. Tinelli, A tale of two solvers : Eager and lazy approaches to bitvectors, Proceedings of the 16th International Conference on Computer Aided Verification, vol.8559, pp.680-695, 2014.

R. Hindley, The principal type-scheme of an object in combinatory logic, Transactions of the American Mathematical Society, vol.146, pp.29-60, 1969.

D. Hoang, Y. Moy, A. Wallenburg, and R. Chapman, SPARK 2014 and GNATprove, International Journal on Software Tools for Technology Transfer, vol.17, issue.6, pp.695-707, 2015.

M. Iguernelala, Strengthening the heart of an SMT-solver : Design and implementation of efficient decision procedures, Theses, Université, 2013.
URL : https://hal.archives-ouvertes.fr/tel-00842555

, Intel Corporation. Intel R 64 and IA-32 Architectures Optimization Reference Manual. Number 248966-041, 2019.

T. A. Junttila and I. Niemelä, Towards an efficient tableau method for boolean circuit satisfiability checking, Computational Logic -CL 2000, pp.553-567, 2000.

L. Khachiyan, Fourier-Motzkin elimination method, pp.1074-1077, 2009.

D. Mentré, C. Marché, J. Filliâtre, M. Asuka, ;. et al., Discharging Proof Obligations from Atelier B Using Multiple Automated Provers, Abstract State Machines, pp.238-251, 2012.

R. Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff : Engineering an efficient sat solver, Proceedings of the 38th Annual Design Automation Conference, DAC '01, pp.530-535, 2001.

L. Moura and N. Bjørner, Efficient e-matching for smt solvers, Proceedings of the 21st International Conference on Automated Deduction : Automated Deduction, CADE-21, pp.183-198, 2007.

G. Nelson and D. C. Oppen, Fast decision procedures based on congruence closure, J. ACM, vol.27, issue.2, pp.356-364, 1980.

R. Nieuwenhuis and A. Oliveras, Fast congruence closure and extensions, Inf. Comput, vol.205, pp.557-580, 2007.

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving sat and sat modulo theories : From an abstract davis-putnam-logemannloveland procedure to dpll(t), J. ACM, vol.53, issue.6, pp.937-977, 2006.

C. Benjamin and . Pierce, Types and Programming Languages, 2002.

S. Ranise and C. Tinelli, The smt-lib format : An initial proposal, PDPAR, pp.94-111, 2003.

S. Ranise and C. Tinelli, The SMT-LIB Standard : Version 1.2, 2006.

J. A. Robinson, A machine-oriented logic based on the resolution principle, J. ACM, vol.12, issue.1, pp.23-41, 1965.

R. E. Shostak, Deciding combinations of theories, J. ACM, vol.31, issue.1, pp.1-12, 1984.

P. M. João, K. A. Silva, and . Sakallah, Grasp&mdash ;a new search algorithm for satisfiability, Proceedings of the, 1996.

, IEEE/ACM International Conference on Computer-aided Design, IC-CAD '96, pp.220-227, 1996.

W. Snyder, Efficient ground completion, Rewriting Techniques and Applications, pp.419-433, 1989.

G. S. Tseitin, On the Complexity of Derivation in Propositional Calculus, pp.466-483, 1983.

A. Voronkov, L. Kovács, G. Reger, and M. Suda,

L. Zhang, C. F. Madigan, M. H. Moskewicz, and S. Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM International Conference on Computer-aided Design, ICCAD '01, pp.279-285, 2001.