Inicio   >   Demostradores   >   ATAME

ATAME

Demostrador|vrain

Descripción
Herramienta online para verificar automáticamente modelos de sistemas (programas) escritos en lenguaje Maude
Miembro
dirección
Camino de Vera S/N
Provincia
Valencia

INFORMACIÓN DEL DEMOSTRADOR

DESCRIPCIÓN

ATAME es una herramienta automática de especialización de programas escritos en el lenguaje Maude que, dados un conjunto de aserciones que modelan el comportamiento deseado de un programa, y un programa que puede violar alguna de estas aserciones, genera automáticamente un programa seguro en el que todas las posibles ejecuciones satisfacen las aserciones planteadas.

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