Cet article présente SolverCheck, une bibliothèque libre de "test par propriétés" (property-based testing, PBT) qui a été spécifiquement conçue pour tester les solveurs CP.
En particulier, SolverCheck offre un langage déclaratif qui permet de décrire le comportement attendu d'un propagateur et de le tester automatiquement.
Ces tests permettent non seulement de s'assurer que le propagateur ne supprime aucune des solutions d'un CSP mais aussi de s'assurer du niveau de consistance imposé par celui-ci (en ce compris, des consistances hybrides, personnalisables). Les expériences réalisées sur AbsCon, Choco, JaCoP et MiniCP ont permi la mise en évidence de bugs non triviaux malgré le grand soin apporté à la confection des suites de tests de ces solveurs.
Cet article a été présenté lors des JFPC 2019 du 12 au 14 juin à Albi, France.
A propos des auteurs :
Xavier Gillard, doctorant à l'UCLouvain, Institut ICTeam son sujet de recherche porte sur "Declarative Testing of Solvers". Il a fait partie du Louvain Verification Lab en tant que doctorant en septembre 2016. Ses recherches visent à comprendre et à exploiter la modularité du contrôle de la satisfaction pour la vérification. Au cours de l'été 2015, Xavier était un étudiant invité du groupe de conception de logiciels du MIT. Auparavant, Xavier a également été actif dans divers domaines de l'industrie allant des télécommunications financières à l'enseignement supérieur et à l'eGovernment.
Pierre Schaus, professeur assistant d'informatique à l'UCLouvain, Institut ICTeam depuis 2012 a obtenu son doctorat de l'Université UCLouvain en 2009. Il a passé 5 mois à l'Université Brown, puis a rejoint la start-up Dynadec pour travailler sur Comet pendant deux ans avant de travailler deux autres années