
infChecker
Demostrador
vrain
Demostrador
vrainMuchas 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.
Ejemplos de uso son: propiedades de seguridad de sistemas concurrentes, no terminación de sistemas de reescritura, verificación de protocolos criptográficos, etc.
Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models