English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

	   This paper introduces  			 		 $\tt{{Presto}}$ 		, a symbolic partial evaluator for Maude’s rewriting logic theories that can improve system analysis and verification. In  			 		 $\tt{{Presto}}$ 		, the automated optimization of a conditional rewrite theory  			 		 $\mathcal{R}$ 		(whose rules define the concurrent transitions of a system) is achieved by partially evaluating, with respect to the rules of  			 		 $\mathcal{R}$ 		, an underlying, companion equational logic theory  			 		 $\mathcal{E}$ 		that specifies the algebraic structure of the system states of  			 		 $\mathcal{R}$ 		. This can be particularly useful for specializing an overly general equational theory  			 		 $\mathcal{E}$ 		whose operators may obey complex combinations of associativity, commutativity, and/or identity axioms, when being plugged into a host rewrite theory  			 		 $\mathcal{R}$ 		as happens, for instance, in protocol analysis, where sophisticated equational theories for cryptography are used.  			 		 $\tt{{Presto}}$ 		implements different unfolding operators that are based on  folding variant narrowing  (the symbolic engine of Maude’s equational theories). When combined with an appropriate abstraction algorithm, they allow the specialization to be adapted to the theory termination behavior and bring significant improvement while ensuring strong correctness and termination of the specialization. We demonstrate the effectiveness of  			 		 $\tt{{Presto}}$ 		in several examples of protocol analysis where it achieves a significant speed-up. Actually, the transformation provided by  			 		 $\tt{{Presto}}$ 		may cut down an infinite folding variant narrowing space to a finite one, and moreover, some of the costly algebraic axioms and rule conditions may be eliminated as well. As far as we know, this is the first partial evaluator for Maude that respects the semantics of functional, logic, concurrent, and object-oriented computations.

Symbolic Specialization of Rewriting Logic Theories with Presto

Symbolic Specialization of Rewriting Logic Theories with `Presto`