- -

Browsing by Author "Meseguer, José"

RiuNet: Institutional repository of the Polithecnic University of Valencia

Browsing by Author "Meseguer, José"

Sort by: Order: Results:

  • thumb
    2D Dependency Pairs for Proving Operational Termination of CTRSs 
    Lucas Alba, Salvador; Meseguer, José (Springer Verlag (Germany), 2014-11)
    The notion of *operational termination* captures nonterminating computations due to subsidiary processes that are necessary to issue a *single* `main' step but which often remain `hidden' when the main computation sequence ...
  • thumb
    A Dependency Pair Framework for AvC-Termination 
    Alarcón Jiménez, Beatriz; Gutiérrez Gil, Raúl; Lucas, Salvador; Meseguer, José (Universitat Politècnica de València, 2011-05-04)
    The development of powerful techniques for proving termination of rewriting modulo a set of equational axioms is essential when dealing with rewriting logic-based programming languages like CafeOBJ, Maude, ELAN, OBJ, etc. ...
  • thumb
    A Modular Order-sorted Equational Generalization Algorithm 
    Alpuente Frasnedo, María; Escobar Román, Santiago; Espert Real, Javier; Meseguer, José (Elsevier, 2014-04)
    Generalization, also called anti-unification, is the dual of unification. Given terms t and t , a generalizer is a term t of which t and t are substitution instances. The dual of a most general unifier (mgu) is that of ...
  • thumb
    A Partial Evaluation Framework for Order-sorted Equational Programs modulo Axioms 
    Alpuente Frasnedo, María; Cuenca-Ortega, Angel Eduardo; Escobar Román, Santiago; Meseguer, José (Elsevier, 2020-01)
    [EN] Partial evaluation is a powerful and general program optimization technique with many successful applications. Existing PE schemes do not apply to expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ...
  • thumb
    ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance 
    Alpuente Frasnedo, María; Escobar Román, Santiago; Espert Real, Javier; Meseguer, José (Springer, 2014)
    Computing generalizers is relevant in a wide spectrum of automated reasoning areas where analogical reasoning and inductive inference are needed. The ACUOS system computes a complete and minimal set of semantic generalizers ...
  • thumb
    ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance (extended version) 
    Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José (Universitat Politècnica de València, 2014-07-16)
    Computing generalizers is relevant in a wide spectrum of automated reasoning areas where analogical reasoning and inductive inference are needed. The ACUOS system computes a complete and minimal set of semantic generalizers ...
  • thumb
    Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis 
    Erbatur, Serdar; Escobar Román, Santiago; Kapur, Deepak; Liu, Zhiqiang; Lynch, Christopher A.; Meadows, Catherine; Meseguer, José; Narendran, Paliath; Santiago Pinazo, Sonia; Sasse, Ralf (Springer, 2013)
    We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition ...
  • thumb
    Dependency pairs for proving termination properties of conditional term rewriting systems 
    Lucas Alba, Salvador; Meseguer, José (Elsevier, 2017-01)
    [EN] The notion of operational termination provides a logic-based definition of termination of computational systems as the absence of infinite inferences in the computational logic describing the operational semantics of ...
  • thumb
    Effective symbolic protocol analysis via equational irreducibility conditions 
    Erbatur, Serdar; Escobar Román, Santiago; Kapur, Deepak; Liu, Zhiqiang; Lynch, Christopher; Meadows, Catherine; Meseguer, José; Narendran, Paliath; Santiago Pinazo, Sonia; Sasse, Ralf (Springer Verlag (Germany), 2012)
    We address a problem that arises in cryptographic protocol analysis when the equational properties of the cryptosystem are taken into account: in many situations it is necessary to guarantee that certain terms generated ...
  • thumb
    Folding variant narrowing and optimal variant termination 
    Escobar Román, Santiago; Sasse, Ralf; Meseguer, José (Elsevier, 2012-11)
    Automated reasoning modulo an equational theory E is a fundamental technique in many applications. If E can be split as a disjoint union E u Ax in such a way that E is confluent, terminating, sort-decreasing, and coherent ...
  • thumb
    Models for logics and conditional constraints in automated proofs of termination 
    Lucas Alba, Salvador; Meseguer, José (Springer Verlag (Germany), 2014)
    Reasoning about termination of declarative programs, which are described by means of a computational logic, requires the definition of appropriate abstractions as semantic models of the logic, and also handling the conditional ...
  • thumb
    Order-sorted Equational Generalization Algorithm Revisited 
    Alpuente Frasnedo, María; Escobar Román, Santiago; Meseguer, José; Sapiña-Sanchis, Julia (Springer-Verlag, 2022-05)
    [EN] Generalization, also called anti-unification, is the dual of unification. A generalizer of two terms t and t' is a term t '' of which t and t' are substitution instances. The dual of most general equational unifiers ...
  • thumb
    Order-sorted Homeomorphic Embedding modulo Combinations of Associativity and/or Commutativity Axioms 
    Alpuente Frasnedo, María; Cuenca-Ortega, Angel; Escobar Román, Santiago; Meseguer, José (IOS Press, 2020)
    [EN] 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 ...
  • thumb
    Protocol analysis modulo combination of theories: A case study in Maude-NPA 
    Sasse, Ralf; Escobar Román, Santiago; Meadows, Catherine; Meseguer, José (Springer Verlag (Germany), 2011)
    There is a growing interest in formal methods and tools to analyze cryptographic protocols modulo algebraic properties of their underlying cryptographic functions. It is well-known that an intruder who uses algebraic ...
  • thumb
    Protocol Analysis with Time 
    Aparicio-Sánchez, Damián; Escobar Román, Santiago; Meadows, Catherine; Meseguer, José; Sapiña-Sanchis, Julia (Springer, 2020-12-16)
    [EN] We present a framework suited to the analysis of cryptographic protocols that make use of time in their execution. We provide a process algebra syntax that makes time information available to processes, and a transition ...
  • Icon
    Proving Operational Termination of Declarative Programs in General Logics 
    Lucas Alba, Salvador; Meseguer, José (ACM, 2014-09)
    A declarative program P is a *theory* in a given computational logic L, so that *computation* with such a program is efficiently implemented as *deduction* in L. That is why *inference systems* are crucial: they both (i) ...
  • thumb
    State space reduction in the Maude-NRL Protocol Analyzer 
    Escobar Román, Santiago; Meadows, Cahterine; Meseguer, José; Santiago Pinazo, Sonia (Elsevier, 2014-11)
    The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and ...
  • thumb
    Strong and weak operational termination of order-sorted rewrite theories 
    Lucas Alba, Salvador; Meseguer, José (Springer Verlag (Germany), 2014-11)
    This paper presents several new results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs) which contains the more restricted framework of conditional term rewriting systems ...
  • thumb
    The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors 
    Lucas Alba, Salvador; Meseguer, José; Gutiérrez Gil, Raúl (Elsevier, 2018-09)
    [EN] 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 ...
  • thumb
    The 2D Dependency Pair Framework for Conditional Rewrite Systems¿Part II: Advanced Processors and Implementation Techniques 
    Lucas Alba, Salvador; Meseguer, José; Gutiérrez Gil, Raúl (Springer-Verlag, 2020-10)
    [EN] Proving termination of programs in `real-life¿ rewriting-based languages like CafeOBJ, Haskell, Maude, etc., is an important subject of research. To advance this goal, faithfully cap- turing the impact in the termination ...