Les techniques de génération automatique de tests ont fait des progrès significatifs pendant les vingt dernières années. Un des succès les plus remarquables dans ce domaine est l'exécution symbolique dynamique (DSE), une technique de génération de tests qui combine l'exécution symbolique et l'exécution concrète du programme sous test. Des travaux récents ont proposé un mécanisme générique pour la spécification des critères de couverture de test à l'aide d'objectifs de test élémentaires, appelés étiquettes de couverture (ou (coverage) labels), ainsi que des solutions pour une génération de tests efficace pour les labels. Cependant, ces techniques n'ont jamais été intégrées dans des générateurs de tests publiquement disponibles. Notre but est de démontrer qu'un support efficace des labels peut être intégré dans Klee, un générateur de tests populaire et ouvert, basé sur la DSE. La version de l'outil réalisée, appelée Klee4labels, est publiquement disponible. Nos expérimentations confirment les avantages de la technique proposée. Cette soumission est un résumé long de l'article publié à SAC-SVT 2023.