, 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
, , pp.35-68, 2007.
Abstract congruence closure, Journal of Automated Reasoning, vol.31, issue.2, pp.129-168, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00099511
Smt-lib 3 : Bringing higher-order logic to smt, 2018. ,
Combining sat methods with non-clausal decision heuristics, Electron. Notes Theor. Comput. Sci, vol.125, issue.3, pp.3-12, 2005. ,
The SMT-LIB Standard : Version 2.5, 2015. ,
The Satisfiability Modulo Theories Library (SMT-LIB), 2016. ,
The SMT-LIB Standard : Version 2.6, 2017. ,
The SMT-LIB Standard : Version 2.0, 2010. ,
The SMT-LIB Standard : Version 2.0, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), 2010. ,
CVC4 : the SMT solver ,
Handbook of Satisfiability : Volume 185 Frontiers in Artificial Intelligence and Ap-Bibliographie plications, 2009. ,
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. ,
Expressing Polymorphic Types in a Many-Sorted Language, pp.87-102 ,
URL : https://hal.archives-ouvertes.fr/inria-00591414
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
Reducing garbage collector cache misses, 2000. ,
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. ,
Memory profiling of OCaml applications. Theses, ENSTA ParisTech, 2014. ,
URL : https://hal.archives-ouvertes.fr/tel-01122262
ocp-memprof : un profileur mémoire pour OCaml, Vingt-sixièmes Journées Francophones des Langages Applicatifs, 2015. ,
A nonrecursive list compacting algorithm, Commun. ACM, vol.13, issue.11, pp.677-678, 1970. ,
Type-safe modular hashconsing, In : Proceedings of the 2006 workshop on ML, pp.12-19, 2006. ,
Canonized rewriting and ground AC completion modulo shostak theories : Design and implementation, Logical Methods in Computer Science, vol.8, issue.3, 2012. ,
Cc(x) : Semantic combination of congruence closure with solvable theories, Electronic Notes in Theoretical Computer Science, vol.198, issue.2, pp.51-69, 2008. ,
Mohamed Iguernelala, and Alain Mebsout, Proceedings of the 16th International Workshop on Satisfiability Modulo Theories, SMT 2018, 2018. ,
A three-tier strategy for reasoning about floating-point numbers in smt, Computer Aided Verification, pp.419-435, 2017. ,
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. ,
Handling polymorphism in automated deduction, 21th International Conference on Automated Deduction (CADE-21), vol.4603, pp.263-278, 2007. ,
Faithful reimplementation of minisat 2.2 in ocaml, 2018. ,
Linear Programming and Extensions, 1991. ,
A machine program for theorem-proving, Commun. ACM, vol.5, issue.7, pp.394-397, 1962. ,
A computing procedure for quantification theory, J. ACM, vol.7, issue.3, pp.201-215, 1960. ,
Z3, an efficient SMT solver ,
Relevancy propagation, 2007. ,
Computing prime implicants, pp.46-52, 2013. ,
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
Simplify : A theorem prover for program checking, J. ACM, vol.52, issue.3, pp.365-473, 2005. ,
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. ,
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
The veriT SMT solver ,
An extensible sat-solver, Theory and Applications of Satisfiability Testing, pp.502-518, 2004. ,
A sat solver for circuits based on the tableau method, vol.24, pp.15-23, 2010. ,
One Logic To Use Them All, CADE 24 -the 24th International Conference on Automated Deduction, 2013. ,
Why3 -where programs meet provers, Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems, pp.125-128, 2013. ,
Why3 -Where Programs Meet Provers, ESOP'13 22nd European Symposium on Programming, vol.7792, 2013. ,
Dpll(t) : Fast decision procedures, vol.06, 2004. ,
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. ,
The principal type-scheme of an object in combinatory logic, Transactions of the American Mathematical Society, vol.146, pp.29-60, 1969. ,
SPARK 2014 and GNATprove, International Journal on Software Tools for Technology Transfer, vol.17, issue.6, pp.695-707, 2015. ,
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.
Towards an efficient tableau method for boolean circuit satisfiability checking, Computational Logic -CL 2000, pp.553-567, 2000. ,
Fourier-Motzkin elimination method, pp.1074-1077, 2009. ,
Discharging Proof Obligations from Atelier B Using Multiple Automated Provers, Abstract State Machines, pp.238-251, 2012. ,
A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978. ,
Chaff : Engineering an efficient sat solver, Proceedings of the 38th Annual Design Automation Conference, DAC '01, pp.530-535, 2001. ,
Efficient e-matching for smt solvers, Proceedings of the 21st International Conference on Automated Deduction : Automated Deduction, CADE-21, pp.183-198, 2007. ,
Fast decision procedures based on congruence closure, J. ACM, vol.27, issue.2, pp.356-364, 1980. ,
Fast congruence closure and extensions, Inf. Comput, vol.205, pp.557-580, 2007. ,
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. ,
Types and Programming Languages, 2002. ,
The smt-lib format : An initial proposal, PDPAR, pp.94-111, 2003. ,
The SMT-LIB Standard : Version 1.2, 2006. ,
A machine-oriented logic based on the resolution principle, J. ACM, vol.12, issue.1, pp.23-41, 1965. ,
Deciding combinations of theories, J. ACM, vol.31, issue.1, pp.1-12, 1984. ,
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.
Efficient ground completion, Rewriting Techniques and Applications, pp.419-433, 1989. ,
On the Complexity of Derivation in Propositional Calculus, pp.466-483, 1983. ,
,
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. ,