Navegación

Búsqueda

Búsqueda avanzada

El autor José Meseguer ha publicado 7 artículo(s):

1 - Proving termination properties of conditional rewrite systems

Conditional Term Rewriting Systems (CTRSs) extend Term Rewriting Systems (TRSs) conditional part c to each rewrite rule l → r, thus obtaining a conditional rewrite rule l → r ⇐ c. The addition of such conditional parts c substantially increases the expressiveness of programming languages that use them and often clarifies the purpose of the rules to make programs more readable and self-explanatory. Computations with CTRSs are defined by means of an Inference System where each rewriting step s →R t requires a proof. This proof-theoretical definition of the operational semantics suggests a natural definition of the termination behavior of R as the absence of infinite proof trees. The notion of operational termination captures this idea, meaning that, given an initial goal, an interpreter will either succeed in finite time in producing a closed proof tree, or will fail in finite time, not being able to close or extend further any of the possible proof trees, after exhaustively searching all such proof trees. Besides implying termination in the usual ‘horizontal’ sense (i.e., as the absence of infinite sequences of rewrite steps), operational termination also captures a ‘vertical’ dimension of the termination behavior which is missing in the usual “without infinite reduction sequences” definition of termination. In [1] we define the notion of V-termination, which captures such a vertical dimension of the termination behavior of CTRSs. We provide a uniform definition of termination and V-termination of CTRSs as the absence of specific kinds of infinite proof trees. We prove that operational termination is just the conjunction of termination and V-termination. We use these results to develop a methodology to prove or disprove termination, V-termination, and operational termination of CTRSs by extending the Dependency Pair (DP) approach for TRSs and generalize the DP approach to all aforementioned termination properties of CTRSs.

Autores: Salvador Lucas / José Meseguer / 
Palabras Clave:

2 - Partial Evaluation of Order-sorted Equational Programs modulo Axioms (Trabajo de alto nivel)

Partial evaluation (PE) is a powerful and general program optimization
technique with many successful applications. However, it has never been investigated
in the context of expressive rule-based languages like Maude, CafeOBJ,
OBJ, ASF+SDF, and ELAN, which support: rich type structures with sorts, subsorts
and overloading; and equational rewriting modulo axioms such as commutativity,
associativity–commutativity, and associativity–commutativity–identity. In
this paper, we illustrate the key concepts by showing how they apply to partial
evaluation of expressive rule-based programs written in Maude. Our partial evaluation
scheme is based on an automatic unfolding algorithm that computes term
variants and relies on equational least general generalization for ensuring global
termination. We demonstrate the use of the resulting partial evaluator for program
optimization on several examples where it shows significant speed-ups.

Autores: María Alpuente / Angel Cuenca-Ortega / Santiago Escobar / José Meseguer / 
Palabras Clave: Equational Rewriting modulo Axioms - Maude - Partial Evaluation - Rewriting Logic

3 - Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 (Tutorial)

This paper introduces some novel features of Maude 2.7. We have added support for: (i) built-in order-sorted unification modulo associativity, commutativity, and identity, (ii) built-in variant generation, (iii) built-in order-sorted unification modulo a finite variant theory, and (iv) symbolic reachability modulo a finite variant theory.

Autores: Francisco Durán / Steven Eker / Santiago Escobar / Narciso Martí-Oliet / José Meseguer / Carolyn Talcott / 
Palabras Clave: associativity commutativity and identity - Maude - narrowing - Order-sorted - unification

4 - The 2D Dependency Pair Framework for conditional rewrite systems (Trabajo ya publicado)

Different termination properties of conditional term rewriting systems have been recently described emphasizing the bidimensional nature of the termination behavior of conditional rewriting. The absence of infinite sequences of rewriting steps (termination in the usual sense), provides the horizontal dimension. The absence of infinitely many attempts to launch the subsidiary processes that are required to check the rule’s condition and perform a single rewriting step has been called V-termination and provides the vertical dimension. We have characterized these properties by means of appropriate notions of dependency pairs and dependency chains. In this paper we introduce a 2D Dependency Pair Framework for automatically proving and disproving all these termination properties. Our implementation of the framework as part of the termination tool MU-TERM and the benchmarks obtained so far suggest that the 2D Dependency Pair Framework is currently the most powerful technique for proving operational termination of conditional term rewriting systems.

Autores: Salvador Lucas / José Meseguer / Raúl Gutiérrez / 
Palabras Clave: Conditional term rewriting - dependency pairs - Operational Termination - Program analysis

5 -

6 - Associative Unification and Symbolic Reasoning Modulo Associativity in Maude

We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unifica- tion problems u =? v such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a finite and complete set of associative unifiers for a fairly large class of unification problems occurring in prac- tice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a warning that such set may be incom- plete. This paper describes this associative unification algorithm imple- mented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrow- ing based symbolic reachability analysis have been extended to deal with associativity.

Autores: Francisco Durán / Steven Eker / Santiago Escobar / Narciso Marti-Oliet / Jose Meseguer / Carolyn Talcott / 
Palabras Clave: associativity - narrowing - Rewriting Logic - unification

7 - Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA

We perform an automated analysis of two devices developed by Yubico: YubiKey, designed to authenticate a user to network-based services, and YubiHSM, Yubico’s hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol analyzer. Although previous work has been done applying formal tools to these devices, there has not been any completely automated analysis. This is not surprising, because both YubiKey and YubiHSM, which make use of cryptographic APIs, involve a number of complex features: (i) discrete time in the form of Lamport clocks, (ii) a mutable memory for storing previously seen keys or nonces, (iii) event-based properties that require an analysis of sequences of actions, and (iv) reasoning modulo exclusive-or. Maude-NPA has provided support for exclusive-or for years but has not provided support for the other three features, which we show can also be supported by using constraints on natural numbers, protocol composition and reasoning modulo associativity. In this work, we have been able to automatically prove security properties of YubiKey and find the known attacks on the YubiHSM, in both cases beyond the capabilities of previous work using the Tamarin Prover due to the need of auxiliary user-defined lemmas and limited support for exclusive-or. Tamarin has recently been endowed with exclusive-or and we have rewritten the original specification of YubiHSM in Tamarin to use exclusive-or, confirming that both attacks on YubiHSM can be carried out by this recent version of Tamarin.

Autores: Antonio Gonzalez-Burgueño / Damian Aparicio / Santiago Escobar / Catherine Meadows / Jose Meseguer / 
Palabras Clave: equational unification - narrowing - protocol analysis - Rewriting Logic - security