Home   >   Demonstrators   >   ATAME

ATAME

Demonstrator|vrain

Description
Online tool to automatically verify system models (programs) written in Maude language.
Member
Address
Camino de Vera S/N
Province
Valencia

DEMONSTRATOR INFORMATION

DESCRIPTION

ATAME is an automatic program specialization tool written in the Maude language that, given a set of assertions that model the desired behavior of a program, and a program that can violate any of these assertions, automatically generates a safe program in which all possible executions satisfy the assertions.

POSSIBILITIES

See in the summary section

TECHNOLOGICAL ENABLER

Artificial Intelligence and Computing
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