Inicio   >   Demostradores   >   PRESTO

PRESTO

Demostrador|vrain

Descripción
Herramienta online para la evaluación parcial de teorías de reescritura escritas en lenguaje Maude.
Miembro
vrain
dirección
Camino de Vera S/N
Provincia
Valencia

INFORMACIÓN DEL DEMOSTRADOR

DESCRIPCIÓN

Presto es un especializador de programas que puede mejorar el análisis y verificación de un sistema modelado como teoría de reescritura en Maude. En Presto, la optimización de una teoría de reescritura R se consigue gracias a la evaluación parcial de su subteoría ecuacional con respecto al conjunto de reglas de R. Esto puede ser especialmente útil para especializar teorías que definen estructuras algebraicas cuyos operadores pueden obedecer combinaciones complejas de los axiomas de asociatividad, conmutatividad y/o identidad como ocurre, por ejemplo, en el caso del análisis de protocolos criptográficos.

POSIBILIDADES

Ver en el apartado del resumen

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