Résumé - Compteage SMT Approximatif au-delà des Domains Discrètes

Compteage SMT Approximatif au-delà des Domains Discrètes

2025-07-24 17:48:13

{"Arijit Shaw","Kuldeep S. Meel"}

{cs.LO,cs.AI}

Le document présente pact, un compteur de modèle SMT pour des formules hybrides qui utilise un comptage de modèle approché basé sur le hachage pour estimer les solutions avec des garanties théoriques. pact effectue un nombre logarithmique d'appels au résolveur SMT par rapport aux variables de projection, en exploitant des fonctions de hachage optimisées. pact atteint des améliorations de performance significatives par rapport aux bases de comparaison sur une large gamme de benchmarks. **Points clés** : * **Comptage SMT** : Le document se concentre sur le comptage SMT, qui consiste à compter le nombre d'assignments satisfaisants pour une formule SMT donnée. Cela représente un problème complexe en raison de la complexité des formules SMT, qui peuvent impliquer à la fois des variables discrètes et continues. * **Formules SMT hybrides** : pact est spécifiquement conçu pour les formules SMT hybrides, qui combinent des variables discrètes et continues. Cela est important pour la modélisation de problèmes du monde réel, tels que les systèmes cyber-physiques et la vérification logicielle. * **Comptage approché basé sur le hachage** : pact utilise un comptage approché basé sur le hachage pour estimer le nombre de solutions. Cette approche implique de diviser l'espace de solutions en cellules à l'aide de fonctions de hachage et de compter le nombre de solutions dans chaque cellule. * **Fonctions de hachage optimisées** : pact utilise des fonctions de hachage optimisées, telles que multiply-mod-prime, multiply-shift et XOR, pour améliorer l'efficacité du processus de comptage. * **Évaluation empirique** : Le document présente une évaluation empirique approfondie de pact sur une large gamme de benchmarks. pact surpasse les bases de comparaison existantes en termes de temps d'exécution et de précision. **Applications** : Le document discute de plusieurs applications motivantes pour pact, y compris : * **Analyse de la robustesse des systèmes cyber-physiques automobiles** : pact peut être utilisé pour analyser la robustesse des systèmes cyber-physiques automobiles en comptant le nombre de vecteurs d'attaque potentiels. * **Analyse de la réachabilité de logiciels critiques** : pact peut être utilisé pour analyser la réachabilité de logiciels critiques en comptant le nombre de chemins satisfaisants dans le graphe de contrôle de flux. * **Vérification logicielle quantitative** : pact peut être utilisé pour quantifier la fiabilité du logiciel en comptant le nombre d'inputs qui conduisent à des échecs d'affirmation. * **Quantification des flux d'information** : pact peut être utilisé pour quantifier les flux d'information dans le logiciel en comptant le nombre de chemins qui conduisent à des fuites d'information. **Conclusion** : Pact est un outil puissant pour le comptage SMT, en particulier pour les formules SMT hybrides. Son évaluation empirique démontre son efficacité et son efficience. pact a le potentiel d'être appliqué à une large gamme de problèmes du monde réel.