Inicio   >   Demostradores   >   INFCHECKER

infChecker

Demostrador|vrain

Descripción
Verificación de fórmulas existenciales en programas basados en reglas de reescritura
Miembro
vrain
dirección
Camino de Vera S/N
Provincia
Valencia

INFORMACIÓN DEL DEMOSTRADOR

DESCRIPCIÓN

Muchas propiedades de programas y sistemas de cómputo representados como teorías lógicas de primer orden pueden formularse como combinaciones booleanas de átomos donde todas las variables están cuantificadas existencialmente. La herramienta infChecker se centra en el análisis de dichas propiedades para lenguajes de programación basados en la reescritura. Su funcionamiento es completamente automático, sin necesidad de que el usuario intervenga más que para proporcionar el problema a tratar. infChecker ha participado con excelentes resultados en competiciones internacionales junto con herramientas de propósito similar.

POSIBILIDADES

Ejemplos de uso son: propiedades de seguridad de sistemas concurrentes, no terminación de sistemas de reescritura, verificación de protocolos criptográficos, etc.

HABILITADOR TECNOLOGICO

Inteligencia Artificial y Computación
Data security and privacy technologies

Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models