
PRESTO
Demonstrator
vrain
Demonstrator
vrainPresto 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.
See in the summary section
Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models