
PRESTO
Demostrador
vrain
Demostrador
vrainPresto 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.
Ver en el apartado del resumen
Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models