Resumen - Conteo Aproximado de SMT en Dominios más Allá del Discreto

Conteo Aproximado de SMT en Dominios más Allá del Discreto

2025-07-24 17:48:13

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

{cs.LO,cs.AI}

El artículo introduce pact, un contador de modelos SMT para fórmulas híbridas que utiliza el conteo aproximado basado en hash para estimar soluciones con garantías teóricas. pact realiza un número logarítmico de llamadas a resolvers SMT en relación con las variables de proyección, aprovechando funciones de hash optimizadas. pact alcanza mejoras significativas en el rendimiento en comparación con los puntos de referencia en una gran suite de pruebas. **Puntos Clave**: * **Conteo SMT**: El artículo se centra en el conteo SMT, que es la tarea de contar el número de asignaciones satisfactorias para una fórmula SMT dada. Este es un problema desafiante debido a la complejidad de las fórmulas SMT, que pueden involucrar variables tanto discretas como continuas. * **Fórmulas SMT Híbridas**: pact está específicamente diseñado para fórmulas SMT híbridas, que combinan variables discretas y continuas. Esto es importante para la modelización de problemas del mundo real, como los sistemas ciber-físicos y la verificación de software. * **Conteo Aproximado Basado en Hashing**: pact utiliza el conteo aproximado basado en hash para estimar el número de soluciones. Este enfoque implica dividir el espacio de soluciones en celdas utilizando funciones de hash y luego contar el número de soluciones en cada celda. * **Funciones de Hash Optimizadas**: pact aprovecha funciones de hash optimizadas, como multiplicar-mod-prime, multiplicar-desplazar y XOR, para mejorar la eficiencia del proceso de conteo. * **Evaluación Empírica**: El artículo presenta una evaluación empírica exhaustiva de pact en una gran suite de pruebas. pact supera a los puntos de referencia existentes en términos de tiempo de ejecución y precisión. **Aplicaciones**: El artículo discute varias aplicaciones motivadoras para pact, entre ellas: * **Análisis de Robustez de Sistemas Ciber-Físicos Automotrices**: pact puede utilizarse para analizar la robustez de sistemas ciber-físicos automotrices al contar el número de vectores de ataque potenciales. * **Análisis de Alcanzabilidad de Software Crítico**: pact puede utilizarse para analizar la alcanzabilidad de software crítico al contar el número de caminos satisfactorios en el grafo de flujo de control. * **Verificación Cuantitativa de Software**: pact puede utilizarse para cuantificar la confiabilidad del software al contar el número de entradas que conducen a fallos de afirmación. * **Cuantificación del Flujo de Información**: pact puede utilizarse para cuantificar el flujo de información en el software al contar el número de caminos que conducen a la fuga de información. **Conclusión**: Pact es una herramienta poderosa para el conteo SMT, especialmente para fórmulas SMT híbridas. Su evaluación empírica demuestra su efectividad y eficiencia. pact tiene el potencial de aplicarse a una amplia gama de problemas del mundo real.