This work presents a narrowing calculus for reachability problems in order-sorted conditional rewrite theories whose underlying equational logic is composed of some theories solvable via a satisfiability modulo theories (SMT) solver plus some combination of associativity, commutativity, and identity axioms for the non-SMT part of the equational logic; the conditions of the rules can be either rewrite conditions or quantifier-free SMT formulas. For any normalized answer of a reachability problem, this calculus computes this answer, or a more general one that can be instantiated to it.

This paper proposes the development of a logic for verifying properties of programs in rewriting logic. Rewriting logic is primarily a logic of change, in which deduction corresponds directly to computation, and not a logic to talk about change in a more indirect and global manner, such as the different modal and temporal logics that can be found in the literature. We start by defining a modal action logic (VLRL) in which rewrite rules are captured as actions. The main novelty of this logic is a topological modality associated with state constructors that allows us to reason about the structure of states, stating that the current state can be decomposed into regions satisfying certain properties. Then, on top of the modal logic, we define a temporal logic for reasoning about properties of the computations generated from rewrite theories, and demonstrate its potential by means of several examples.

Abstract. We present three descriptions, at different abstract levels, of the tree identify protocol from the IEEE 1394 serial multimedia bus standard. The descriptions are given using the language Maude based on rewriting logic. Particularly, the time aspects of the protocol are studied. We prove the correctness of the protocol in two steps. First, the descriptions are validated by an exhaustive exploration of all the possible states reachable from an initial configuration of a network, checking that always only one leader is chosen. Then, we give a formal proof showing that the desirable properties of the protocol are always fulfilled by any network, provided that the network is connected and acyclic.