
Abets
Demostrador
vrain
Demostrador
vrainABETS es un analizador dinámico basado en aserciones que automáticamente computa vistas abstractas de ejecuciones Maude. ABETS está compuesto sobre un versátil fragmentador de programas y emplea verificación de aserciones en tiempo de ejecución para mejorar el análisis dinámico. ABETS puede ser usado para mejorar el diagnóstico de errores en modelos (programas) escritos en Maude simplificando automáticamente el tamaño y complejidad de los programas analizados y sus trazas. Las principales fortalezas de la herramienta son: (i) detección automática de comportamientos de programa erróneos con respecto a un conjunto de aserciones, (ii) inferencia automática de criterios de fragmentación precisos para los errores detectados y (iii) generación automática de contraejemplos simplificados.
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