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.

The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equational axioms. This paper generalizes the symbolic homeomorphic embedding relation to order–sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of different, increasingly efficient formulations of the homeomorphic embedding relation modulo axioms that we implement in Maude. Our experimental results show that the most efficient version indeed pays off in practice.

In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KERNELC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KERNELC in the 𝕂 semantic framework, we enrich the symbolic execution facilities recently provided by 𝕂 with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KINDSPEC 2.1, which generates logical axioms that express pre- and post-condition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by 𝕂, some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our setting with little effort.

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 This paper introducesGLINTS, a graphical tool for exploring variant narrowing computations in Maude. The most recent version of Maude, version 2.7.1, provides quite sophisticated unification features, including order-sorted equational unification for convergent theories modulo axioms such as associativity, commutativity, and identity. This novel equational unification relies on built-in generation of the set ofvariantsof a termt, i.e., the canonical form oftσ for a computed substitution σ. Variant generation relies on a novel narrowing strategy calledfolding variant narrowingthat opens up new applications in formal reasoning, theorem proving, testing, protocol analysis, and model checking, especially when the theory satisfies thefinite variant property, i.e., there is a finite number of most general variants for every term in the theory. However, variant narrowing computations can be extremely involved and are simply presented in text format by Maude, often being too heavy to be debugged or even understood. TheGLINTSsystem provides support for (i) determining whether a given theory satisfies the finite variant property, (ii) thoroughly exploring variant narrowing computations, (iii) automatic checking of nodeembeddingandclosednessmodulo axioms, and (iv) querying and inspecting selected parts of the variant trees.

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.

Formal specifications can be used for various software engineering activities ranging from finding errors to documenting software and automatic test-case generation. Automatically discovering specifications for heap-manipulating programs is a challenging task. In this paper, we propose a technique for automatically inferring formal specifications from C code which is based on the symbolic execution and automated reasoning tandem "Matching Logic/K framework". We implemented our technique for a fragment of C called KernelC, in the automated tool KingSpec, which generates axioms that describe the precise input/output behavior of C routines that handle pointer-based structures, i.e., result values and state change. These specifications can be written either in Matching Logic itself, which is useful for further automated analysis within the K formal environment, or in sugared axiomatic form, which favors better human inspection. Since we rely on rewriting logic K semantics specification of programming languages, our approach can be easily extended to any language for which %that a formal semantics in K is given.

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.

Abstract The application of automatic transformation processes during the formal development and optimization of programs can introduce encumbrances in the generated code that programmers usually (or presumably) do not write. An example is the introduction of redundant arguments in the functions defined in the program. Redundancy of a parameter means that replacing it by any expression does not change the result. In this work, we provide methods for the analysis and elimination of redundant arguments in term rewriting systems as a model for the programs that can be written in more sophisticated languages. On the basis of the uselessness of redundant arguments, we also propose an erasure procedure which may avoid wasteful computations while still preserving the semantics (under ascertained conditions). A prototype implementation of these methods has been undertaken, which demonstrates the practicality 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

Many functional logic languages are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction mechanism of functional languages and the resolution principle of logic languages. Needed narrowing is an optimal evaluation strategy which constitutes the basis of modern (narrowing-based) lazy functional logic languages. In this work, we present the fundamentals of partial evaluation in such languages. We provide correctness results for partial evaluation based on needed narrowing and show that the nice properties of this strategy are essential for the specialization process. In particular, the structure of the original program is preserved by partial evaluation and, thus, the same evaluation strategy can be applied for the execution of specialized programs. This is in contrast to other partial evaluation schemes for lazy functional logic programs which may change the program structure in a negative way. Recent proposals for the partial evaluation of declarative multi-paradigm programs use (some form of) needed narrowing to perform computations at partial evaluation time. Therefore, our results constitute the basis for the correctness of such partial evaluators.

Needed narrowing is a complete and optimal operational principle for modern declarative languages which integrate the best features of lazy functional and logic programming. We investigate the formal relation between needed narrowing and another (not so lazy) narrowing strategy which is the basis for popular implementations of lazy functional logic languages. We demonstrate that needed narrowing and lazy narrowing are computationally equivalent over the class of uniform programs. We also introduce a complete refinement of lazy narrowing, called uniform lazy narrowing, which is still equivalent to needed narrowing over the aforementioned class. Since actual implementations of functional logic languages are based on the transformation of the original program into a uniform one—which is then executed using a lazy narrowing strategy—our results can be thought of as a formal basis for the correctness of these implementations.

Functional logic languages combine the operational principles of the most important declarative programming paradigms, namely functional and logic programming. Inductively sequential programs admit the definition of optimal computation strategies and are the basis of several recent (lazy) functional logic languages. In this paper, we define a partial evaluator for inductively sequential functional logic programs. We prove strong correctness of this partial evaluator and show that the nice properties of inductively sequential programs carry over to the specialization process and the specialized programs. In particular, the structure of the programs is preserved by the specialization process. This is in contrast to other partial evaluation methods for functional logic programs which can destroy the original program structure. Finally, we present some experiments which highlight the practical advantages of our approach.

Languages that integrate functional and logic programming with a complete operational semantics are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction principle of functional languages and the resolution principle of logic languages. In this article, we present a partial evaluation scheme for functional logic languages based on an automatic unfolding algorithm which builds narrowing trees. The method is formalized within the theoretical framework established by Lloyd and Shepherdson for the partial deduction of logic programs, which we have generalized for dealing with functional computations. A generic specialization algorithm is proposed which does not depend on the eager or lazy nature of the narrower being used. To the best of our knowledge, this is the first generic algorithm for the specialization of functional logic programs. We also discuss the relation to work on partial evaluation in functional programming, term-rewriting systems, and logic programming. Finally, we present some experimental results with an implementation of the algorithm which show in practice that the narrowing-driven partial evaluator effectively combines the propagation of partial data structures (by means of logical variables and unification) with better opportunities for optimization (thanks to the functional dimension).

Partial evaluation is a method for program specialization based on fold/unfold transformations [8, 25]. Partial evaluation of pure functional programs uses mainly static values of given data to specialize the program [15, 44]. In logic programming, the so-called static/dynamic distinction is hardly present, whereas considerations of determinacy and choice points are far more important for control [12]. We discuss these issues in the context of a (lazy) functional logic language. We formalize a two-phase specialization method for a non-strict, first order, integrated language which makes use of lazy narrowing to specialize the program w.r. t. a goal. The basic algorithm (first phase) is formalized as an instance of the framework for the partial evaluation of functional logic programs of [2, 3], using lazy narrowing. However, the results inherited by [2, 3] mainly regard the termination of the PE method, while the (strong) soundness and completeness results must be restated for the lazy strategy. A post-processing renaming scheme (second phase) is necessary which we describe and illustrate on the well-known matching example. This phase is essential also for other non-lazy narrowing strategies, like innermost narrowing, and our method can be easily extended to these strategies. We show that our method preserves the lazy narrowing semantics and that the inclusion of simplification steps in narrowing derivations can improve control during specialization.