In this paper, we develop an automated optimization framework for rewrite theories that supports sorts, subsort overloading, equations and algebraic axioms with free/non-free constructors, and rewrite rules modeling concurrent system transitions whose state structure is defined by means of the equations. The main idea of the framework is to make the system computations more efficient by partially evaluating the equations to the specific calls that are required by the transition rules. This can be particularly useful for automatically optimizing rewrite theories that contain overly general equational theories which perform unnecessary and costly computations involving pattern matching and/or unification modulo equations and axioms. The transformation is based on a suitable unfolding operator parameter that relies on the symbolic operational engine of Maude's equational theories, called folding variant narrowing, together with a generic abstraction operator. Depending on the properties of the rewrite theory, the unfolding and abstraction operators must be fine-tuned to achieve the biggest optimization possible while ensuring termination and total correctness of the transformation. We formalize two instances of our scheme for the case when the rewrite theory either has an infinite number of most general variants or a finite number of most general variants. Finally, we discuss some experimental results which demonstrate that the proposed optimization technique pays off in practice.

Abstract 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 onfolding 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.

Abstract Concurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude’s symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis in rewrite theories. Intricate computing problems may be effectively and naturally solved in Maude thanks to the synergy of these recently developed symbolic capabilities and classical Maude features, such as: (i) rich type structures with sorts (types), subsorts, and overloading; (ii) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity; and (iii) classical reachability analysis in rewrite theories. However, the combination of all of these features may hinder the understanding of Maude symbolic computations for non-experienced developers. The purpose of this article is to describe how programming and analysis of Maude rewrite theories can be made easier by providing a sophisticated graphical tool called Narval that supports the fine-grained inspection of Maude symbolic computations.

Abstract We presentABETS, an assertion-based, dynamic analyzer that helps diagnose errors in Maude programs.ABETSuses slicing to automatically create reduced versions of both a run's execution trace and executed program, reduced versions in which any information that is not relevant to the bug currently being diagnosed is removed. In addition,ABETSemploys runtime assertion checking to automate the identification of bugs so that whenever an assertion is violated, the system automatically infers accurate slicing criteria from the failure. We summarize the main services provided byABETS, which also include a novel assertion-based facility for program repair that generates suitable program fixes when a state invariant is violated. Finally, we provide an experimental evaluation that shows the performance and effectiveness of the system.

Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we present a fold/unfold-based transformation framework for rewriting logic theories which is based on narrowing. For the best of our knowledge, this is the first fold/unfold transformation framework which allows one to deal with functions, rules, equations, sorts, and algebraic laws (such as commutativity and associativity). We provide correctness results for the transformation system w.r.t. the semantics of ground reducts. Moreover, we show how our transformation technique can be naturally applied to implement a Code Carrying Theory (CCT) system. CCT is an approach for securing delivery of code from a producer to a consumer where only a certificate (usually in the form of assertions and proofs) is transmitted from the producer to the consumer who can check its validity and then extract executable code from it. Within our framework, the certificate consists of a sequence of transformation steps which can be applied to a given consumer specification in order to automatically synthesize safe code in agreement with the original requirements. We also provide an implementation of the program transformation framework in the high-performance, rewriting logic language Maude which, by means of an experimental evaluation of the system, highlights the potentiality of our approach.

In this paper, we present an extension of PHIL, a declarative language for filtering information from XML data. The proposed approach allows us to extract relevant data as well as to exclude useless and misleading contents from an XML document. Essentially, it combines ontology reasoning with an approximate pattern-matching engine which searches for patterns in a flexible way (i.e. modulo renaming, insertion, and deletion of XML items) and ranks the results w.r.t. their cost. The filtering process is guided by the syntax as well as the semantics of the XML documents, since it relies on both the document structure and the onto- logical information to which the document is related. Such information is retrieved by querying (possibly remote) ontology reasoners. Our methodology has been implemented in the XPHIL system, which is written in Haskell. By using the XML benchmarking tool xmlgen, we have developed some scalable experiments which demonstrate the usefulness of our approach.

The development and maintenance of Web sites are difficult tasks. To maintain the consistency of ever-larger, complex Web sites, Web administrators need effective mechanisms that assist them in fixing every possible inconsistency. In this paper, we present a novel methodology for semi-automatically repairing faulty Web sites which can be integrated on top of an existing rewriting-based verification technique developed in a previous work. Starting from a categorization of the kinds of errors that can be found during the Web verification activities, we formulate a stepwise transformation procedure that achieves correctness and completeness of the Web site w.r.t. its formal specification while respecting the structure of the document (e.g. the schema of an XML document). Finally, we shortly describe a prototype implementation of the repairing tool which we used for an experimental evaluation of our method