Invited Talks

Rewriting, Inference, and Proof

Abstract

Rewriting is a form of inference, and one that interacts in several ways with other forms of inference such as decision procedures and proof search. We discuss a range of issues at the intersection of rewriting and inference. How can other inference procedures be combined with rewriting? Can rewriting be used to describe inference procedures? What are some of the theoretical challenges and practical applications of combining rewriting and inference? How can rewriters, decision procedures, and their combination be certified? We discuss these problems in the context of our ongoing effort to use PVS as a metatheoretic framework to construct a proof kernel for justifying the claims of theorem provers, rewriters, model checkers, and satisfiability solvers.

Natarajan Shankar

Twenty Years of Rewriting Logic

Abstract

The first three papers on rewriting logic were published in 1990 [4,3,2]; they were then expanded in [5,6]. Since that time, many researchers around the world have made important contributions to its foundations, tools, and applications. Since 1996, the WRLA workshop has met biennially, with the 2010 Paphos meeting being its eighth edition, and many hundreds of papers have been published on the subject (for a bibliography up to 2002 see [1]).

José Meseguer

Termination and Narrowing

Proving Termination in the Context-Sensitive Dependency Pair Framework

Abstract

Termination of context-sensitive rewriting (CSR) is an interesting problem with several applications in the fields of term rewriting and in the analysis of programming languages like CafeOBJ, Maude, OBJ, etc. The dependency pair approach, one of the most powerful techniques for proving termination of rewriting, has been adapted to be used for proving termination of CSR. The corresponding notion of context-sensitive dependency pair (CSDP) is different from the standard one in that collapsing pairs (i.e., rules whose right-hand side is a variable) are considered. Although the implementation and practical use of CSDPs lead to a powerful framework for proving termination of CSR, handling collapsing pairs is not easy and often leads to impose heavy requirements over the base orderings which are used to achieve the proofs. A recent proposal removes collapsing pairs by transforming them into sets of new (standard) pairs. In this way, though, the role of collapsing pairs for modeling context-sensitive computations gets lost. This leads to a less intuitive and accurate description of the termination behavior of the system. In this paper, we show how to get the best of the two approaches, thus obtaining a powerful context-sensitive dependency pair framework which satisfies all practical and theoretical expectations.

Raúl Gutiérrez, Salvador Lucas

A Dependency Pair Framework for A ∨ C-Termination

Abstract

The development of powerful techniques for proving termination of rewriting modulo a set of equations is essential when dealing with rewriting logic-based programming languages like CafeOBJ, Maude, OBJ, etc. One of the most important techniques for proving termination over a wide range of variants of rewriting (strategies) is the dependency pair approach. Several works have tried to adapt it to rewriting modulo associative and commutative (AC) equational theories, and even to more general theories. However, as we discuss in this paper, no appropriate notion of minimality (and minimal chain of dependency pairs) which is well-suited to develop a dependency pair framework has been proposed to date. In this paper we carefully analyze the structure of infinite rewrite sequences for rewrite theories whose equational part is a (free) combination of associative and commutative axioms which we call A ∨ C-rewrite theories. Our analysis leads to a more accurate and optimized notion of dependency pairs through the new notion of stably minimal term. Then, we have developed a suitable dependency pair framework for proving termination of A ∨ C-rewrite theories.

Beatriz Alarcón, Salvador Lucas, José Meseguer

Folding Variant Narrowing and Optimal Variant Termination

Abstract

If a set of equations E ∪ Ax is such that E is confluent, terminating, and coherent modulo Ax, narrowing with E modulo Ax provides a complete E ∪ Ax-unification algorithm. However, except for the hopelessly inefficient case of full narrowing, nothing seems to be known about effective narrowing strategies in the general modulo case beyond the quite depressing observation that basic narrowing is incomplete modulo AC. In this work we propose an effective strategy based on the idea of the E ∪ Ax-variants of a term that we call folding variant narrowing. This strategy is complete, both for computing E ∪ Ax-unifiers and for computing a minimal complete set of variants for any input term. And it is optimally variant terminating in the sense of terminating for an input term t iff t has a finite, complete set of variants. The applications of folding variant narrowing go beyond providing a complete E ∪ Ax-unification algorithm: computing the E ∪ Ax-variants of a term may be just as important as computing E ∪ Ax-unifiers in recent applications of folding variant narrowing such as termination methods modulo axioms, and checking confluence and coherence of rules modulo axioms.

Santiago Escobar, Ralf Sasse, José Meseguer

Tools

A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications

Abstract

The Church-Rosser property, together with termination, is essential for an equational specification to have good executability conditions, and also for having a complete agreement between the specification’s initial algebra, mathematical semantics, and its operational semantics by rewriting. Checking this property for expressive specifications that are order-sorted, conditional with possibly extra variables in their condition, and whose equations can be applied modulo different combinations of associativity, commutativity and identity axioms is challenging. In particular, the resulting conditional critical pairs that cannot be joined have often an intuitively unsatisfiable condition or seem intuitively joinable, so that sophisticated tool support is needed to eliminate them. Another challenge is the presence of different combinations of associativity, commutativity and identity axioms, including the very challenging case of associativity without commutativity for which no finitary unification algorithms exist. In this paper we present the foundations and illustrate the design and use of a completely new version of the Maude Church-Rosser Checker tool that addresses all the above-mentioned challenges and can deal effectively with complex conditional specifications modulo axioms.

Francisco Durán, José Meseguer

A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories

Abstract

For a rewrite theory to be executable, its equations E should be (ground) confluent and terminating modulo the given axioms A, and their rules should be (ground) coherent with E modulo A. The correctness of many important formal verification tasks, including search, LTL model checking, and the development of abstractions, crucially depends on the theory being ground coherent. Furthermore, many specifications of interest are typed, have equations E and rules R that are both conditional, have axioms A involving various combinations of associativity, commutativity and identity, and may contain frozenness restrictions. This makes it essential to extend the known coherence checking methods from the untyped, unconditional, and AC or free case, to this much more general setting. We present the mathematical foundations of the Maude ChC 3 tool, which provide such a generalization to support coherence and ground coherence checking for order-sorted rewrite theories under these general assumptions. We also explain and illustrate the use of the ChC 3 tool with a nontrivial example.

Francisco Durán, José Meseguer

The K Framework

K-Maude: A Rewriting Based Tool for Semantics of Programming Languages

Abstract

K is a rewriting-based framework for defining programming languages. K-Maude is a tool implementing K on top of Maude. K-Maude provides an interface accepting K modules along with regular Maude modules and a collection of tools for transforming K language definitions into Maude rewrite theories for execution or analysis, or into LaTeX for documentation purposes. The current K-Maude prototype was successfully used in defining several languages and language analysis tools, both for research and for teaching purposes. This paper describes the K-Maude tool, both from a user and from an implementer perspective.

Traian Florin Şerbănuţă, Grigore Roşu

Collecting Semantics under Predicate Abstraction in the K Framework

Abstract

The K framework is a specialization of rewriting logic for defining programming language semantics. This paper introduces the model checking with predicate abstraction technique into the K framework. To express this technique in K, we go to the foundations of predicate abstraction, that is abstract interpretation, and use its collecting semantics. As such, we propose a suitable description in K for collecting semantics under predicate abstraction of a simple imperative language. Next, we prove that our K specification for collecting semantics is a sound approximation of the K specification for concrete semantics. This work makes a further step towards the development of program verification methodologies in rewriting logic semantics project in general and the K framework in particular.

Irina Măriuca Asăvoae, Mihail Asăvoae

Applications and Semantics

Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuits

Abstract

Modern asynchronous digital circuits are highly concurrent systems composed largely of customized gates, and can be elegantly modeled using the language of production rules (PRs). One of the present limitations of the state of the art in asynchronous circuit design is that no formal executable semantics of asynchronous circuits has yet been given at the PR level. The primary contribution of this paper is to define, using rewriting logic and Maude, an executable formal semantics of asynchronous circuits at the PR level under three common timing assumptions. Our semantics provides a circuit designer with a PR-level circuit interpreter and with a decision procedure for checking key circuit properties, including hazard-freedom and deadlock-freedom. We describe several reductions and optimizations that can be used to reduce the state space of circuits in our formal semantics and investigate the impact of these reductions experimentally. The analysis scales up to circuits of over 100 PRs in spite of the high levels of concurrency involved.

Michael Katelman, Sean Keller, José Meseguer

A Formal Pattern Architecture for Safe Medical Systems

Abstract

Design patterns have demonstrated major practical uses for cost savings and modular design in software engineering. For safety-critical systems, however, such patterns should also provide formal guarantees that critical safety properties are met. We leverage the power of rewriting logic and parameterization available in Real-Time Maude to add a formal basis for analysis of a novel safety pattern for medical devices. We demonstrate practicality and applicability of our pattern by instantiating it to a pacemaker specification, and we validate our pattern by verifying the safety invariant in the pacemaker instantiation.

Mu Sun, José Meseguer, Lui Sha

On the Behavioral Semantics of Real-Time Domain Specific Visual Languages

Abstract

Domain specific visual languages (DSVLs) are becoming commonplace for specifying systems at a high-level of abstraction, using a notation very close to the problem domain and quite intuitive for domain experts. Usually, DSVLs are defined only in terms of their abstract and concrete syntaxes, with no precise semantics—something that may hamper the use of tools to simulate or analyze the produced models. In this paper we show how rewriting logic, and in particular Real-Time Maude, can be effectively used to provide semantics to real-time DSVLs, and how these Maude specifications can be automatically generated from the visual specifications. The use of Real-Time Maude provides additional interesting benefits, such as being able to simulate the DSVL specifications or to conduct formal analysis on them.

José E. Rivera, Francisco Durán, Antonio Vallecillo

Multiset Rewriting: A Semantic Framework for Concurrency with Name Binding

Abstract

We revise multiset rewriting with name binding, by combining the two main existing approaches to the study of concurrency by means of multiset rewriting: multiset rewriting with existential quantification and constrained multiset rewriting. We obtain ν-MSRs, where we rewrite multisets of atomic formulae, in which some names may be restricted. We prove that ν-MSRs are equivalent to a class of Petri nets in which tokens are tuples of pure names, called pν-APNs. Then we encode π-calculus processes into ν-MSRs in a very direct way, that preserves the topology of bound names, by using the concept of derivatives of a π-calculus process. Finally, we discuss how the recent results on decidable subclasses of the π-calculus are independent of the particular reaction rule of the π-calculus, so that they can be obtained in the more general framework of ν-MSRs. Thus, those results carry over not only to the π-calculus, but to any other formalism that can be encoded within it, as pν-APNs.

Fernando Rosa-Velardo

Maude Model Checking and Debugging

The Linear Temporal Logic of Rewriting Maude Model Checker

Abstract

This paper presents the foundation, design, and implementation of the Linear Temporal Logic of Rewriting model checker as an extension of the Maude system. The Linear Temporal Logic of Rewriting (LTLR) extends linear temporal logic with spatial action patterns which represent rewriting events. LTLR generalizes and extends various state-based and event-based logics and aims to avoid certain types of mismatches between a system and its temporal logic properties. We have implemented the LTLR model checker at the C++ level within the Maude system by extending the existing Maude LTL model checker. Our LTLR model checker provides very expressive methods to define event-related properties as well as state-related properties, or, more generally, properties involving both events and state predicates. This greater expressiveness is gained without compromising performance, because the LTLR implementation minimizes the extra costs involved in handling the events of systems.

Kyungmin Bae, José Meseguer

Enhancing the Debugging of Maude Specifications

Abstract

Declarative debugging is a semi-automatic technique that locates a program fragment responsible for the error by building a tree representing the computation and guiding the user through it to find the error. Two different kinds of errors are considered for debugging: wrong answers—a wrong result obtained from an initial value—and missing answers—a term that should be reachable but cannot be obtained from an initial value—, where the latter has only been considered in nondeterministic systems. However, we consider that missing answers can also appear in deterministic systems, when we obtain correct results that do not provide all the expected information, which corresponds, in the context of Maude modules, to terms whose normal form is not reached and to terms whose computed least sort is, although correct, bigger than the expected one. We present in this paper a calculus to deduce normal forms and least sorts, and a proper abbreviation of the trees obtained with it. These trees increase both the causes (missing equations and memberships) and the errors (erroneous normal forms and least sorts) detected in our debugging framework.

Adrian Riesco, Alberto Verdejo, Narciso Martí-Oliet

Rewrite Engines

The Third Rewrite Engines Competition

Abstract

This paper presents the main results and conclusions of the Third Rewrite Engines Competition (REC III). This edition of the competition took place as part of the 8th Workshop on Rewriting Logic and its Applications (WRLA 2010), and the systems ASF+SDF, Maude, Stratego/XT, Tom, and TXL participated in it.

Francisco Durán, Manuel Roldán, Jean-Christophe Bach, Emilie Balland, Mark van den Brand, James R. Cordy, Steven Eker, Luc Engelen, Maartje de Jonge, Karl Trygve Kalleberg, Lennart C. L. Kats, Pierre-Etienne Moreau, Eelco Visser

Springer Professional

Rewriting Logic and Its Applications

8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers

Inhaltsverzeichnis

Frontmatter

Invited Talks

Rewriting, Inference, and Proof

Twenty Years of Rewriting Logic

Termination and Narrowing

Proving Termination in the Context-Sensitive Dependency Pair Framework

A Dependency Pair Framework for A ∨ C-Termination

Folding Variant Narrowing and Optimal Variant Termination

Tools

A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications

A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories

The K Framework

K-Maude: A Rewriting Based Tool for Semantics of Programming Languages

Collecting Semantics under Predicate Abstraction in the K Framework

Applications and Semantics

Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuits

A Formal Pattern Architecture for Safe Medical Systems

On the Behavioral Semantics of Real-Time Domain Specific Visual Languages

Multiset Rewriting: A Semantic Framework for Concurrency with Name Binding

Maude Model Checking and Debugging

The Linear Temporal Logic of Rewriting Maude Model Checker

Enhancing the Debugging of Maude Specifications

Rewrite Engines

The Third Rewrite Engines Competition

Backmatter