Home   >   Demonstrators   >   PRESTO

PRESTO

Demonstrator|vrain

Description
Online tool for the partial evaluation of rewriting theories written in Maude language.
Member
vrain
Address
Camino de Vera S/N
Province
Valencia

DEMONSTRATOR INFORMATION

DESCRIPTION

Presto is a program specializer that can improve the analysis and verification of a system modeled as a rewrite theory in Maude. In Presto, the optimization of a rewriting theory R is achieved thanks to the partial evaluation of its equational subtheory with respect to the set of rules of R. This can be especially useful to specialize theories that define algebraic structures whose operators may obey complex combinations of the axioms of associativity, commutativity and/or identity as it happens, for example, in the case of the analysis of cryptographic protocols.

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