Home   >   Demonstrators   >   ABETS

Abets

Demonstrator|vrain

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

DEMONSTRATOR INFORMATION

DESCRIPTION

ABETS is an assertion-based dynamic parser that automatically computes abstract views of Maude executions. ABETS is built on top of a versatile program fragmenter and employs run-time assertion checking to improve dynamic analysis. ABETS can be used to improve error diagnosis in models (programs) written in Maude by automatically simplifying the size and complexity of the analyzed programs and their traces. The main strengths of the tool are: (i) automatic detection of erroneous program behavior with respect to a set of assertions, (ii) automatic inference of accurate fragmentation criteria for the detected errors, and (iii) automatic generation of simplified counterexamples.

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