- -

Listar por autor "Lucas Alba, Salvador"

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Listar por autor "Lucas Alba, Salvador"

Ordenar por:Orden:Resultados:

  • 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
    Applications and extensions of context-sensitive rewriting 
    Lucas Alba, Salvador (Elsevier, 2021-06)
    [EN] Context-sensitive rewriting is a restriction of term rewriting which is obtained by imposing replacement restrictions on the arguments of function symbols. It has proven useful to analyze computational properties of ...
  • thumb
    Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories 
    Lucas Alba, Salvador; Gutiérrez Gil, Raúl (Springer-Verlag, 2018)
    [EN] In program analysis, the synthesis of models of logical theories representing the program semantics is often useful to prove program properties. We use order-sorted first- order logic as an appropriate framework to ...
  • thumb
    Automatically Proving and Disproving Feasibility Conditions 
    Gutiérrez Gil, Raúl; Lucas Alba, Salvador (Springer Nature, 2020-07-06)
    [EN] In the realm of term rewriting, given terms s and t, a reachability condition s>>t is called feasible if there is a substitution O such that O(s) rewrites into O(t) in zero or more steps; otherwise, it is ...
  • Icon
    Completeness of Context-Sensitive Rewriting 
    Lucas Alba, Salvador (Elsevier, 2015-02)
    Restrictions of rewriting may turn normal forms of some terms unreachable, leading to incomplete computations. Context-sensitive rewriting (csr) is the restriction of rewriting that only permits reductions on arguments ...
  • thumb
    CONFident: una herramienta para el análisis de la confluencia de sistemas de reescritura 
    Vítores Vicente, Miguel (Universitat Politècnica de València, 2022-04-29)
    [ES] CONFident es una herramienta que demuestra la confluencia, una de las propiedades más importantes en el análisis de sistemas de reescritura. Para ello hace uso de algunas herramientas como infChecker o mu-term. Por ...
  • thumb
    Context-Sensitive Dependency Pairs 
    Alarcón, Beatriz; Gutiérrez Gil, Raúl; Lucas Alba, Salvador (Springer-Verlag, 2006)
    [EN] Termination is one of the most interesting problems when dealing with context-sensitive rewrite systems. Although there is a good number of techniques for proving termination of context-sensitive rewriting (CSR), the ...
  • thumb
    Context-Sensitive Dependency Pairs 
    Alarcón, Beatriz; Gutiérrez Gil, Raúl; Lucas Alba, Salvador (Elsevier, 2010-08)
    [EN] Termination is one of the most interesting problems when dealing with context-sensitive rewrite systems. Although a good number of techniques for proving termination of context-sensitive rewriting (CSR) have been ...
  • thumb
    Context-Sensitive Dependency Pairs Framework 
    Gutiérrez Gil, Raúl (Universitat Politècnica de València, 2011-11-28)
    We show how to develop a dependency pair framework for proving termination of context-sensitive rewriting.
  • Icon
    Context-sensitive Rewriting 
    Lucas Alba, Salvador (Association for Computing Machinery, 2020-09)
    [EN] The appropriate selection of the arguments of functions that can be evaluated in function calls is often useful to improve efficiency, speed, termination behavior, and so on. This is essential, e.g., in the conditional ...
  • 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
    Derivational Complexity and Context-Sensitive Rewriting 
    Lucas Alba, Salvador (Springer-Verlag, 2021-12)
    [EN] Context-sensitive rewriting is a restriction of rewriting where reduction steps are allowed on specific arguments mu(f) subset of {1, ..., k} of k-ary function symbols f only. Terms which cannot be further rewritten ...
  • thumb
    Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting 
    Gutiérrez Gil, Raúl; Lucas Alba, Salvador (Universitat Politècnica de València, 2015-05-26)
    Context-sensitive rewriting (CSR) is a variant of rewriting where only selected arguments of function symbols can be rewritten. Consequently, the subterm positions of a term are classified as either active, i.e., positions ...
  • thumb
    Gestión del consumo energético en el desarrollo de aplicaciones para dispositivos móviles 
    Fresneda González, Sergio (Universitat Politècnica de València, 2017-10-27)
    Personal mobile devices like smartwatches, smartphones, tablets, etc., are just small computers with a computing performance which is similar to last-decade desktop computers. In sharp contrast, though, mobile devices ...
  • thumb
    Implementing high-performance interpreted languages through the use of FPGAs. A proof of concept 
    González Castiñeiras, Daniel (Universitat Politècnica de València, 2024-10-21)
    [EN] The exponential growth of hardware resources in recent decades has led to substantial software bloat, fostering the development of high-level programming languages that prioritize development efficiency over execution ...
  • thumb
    Improving Context-Sensitive Dependency Pairs 
    Alarcón, Beatriz; Emmes, Fabian; Fuhs, Carsten; Giesl, Jürgen; Gutiérrez Gil, Raúl; Lucas Alba, Salvador; Schneider-Kamp, Peter; Thiemann, René (Springer-Verlag, 2008)
    [EN] Context-sensitive dependence pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context-sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from ...
  • thumb
    Improving the Context-Sensitive Dependency Graph 
    Alarcón, Beatriz; Gutiérrez Gil, Raúl; Lucas Alba, Salvador (Elsevier, 2007-07-16)
    [EN] The dependency pairs method is one of the most powerful technique for proving termination of rewriting and it is currently central in most automatic termination provers. Recently, it has been adapted to be used in ...
  • thumb
    infChecker. A Tool for Checking Infeasibility 
    Gutiérrez Gil, Raúl; Lucas Alba, Salvador (Universidade de Brasilia, 2019-06-28)
    [EN] Given a Conditional Term Rewriting System (CTRS) R and terms s and t, we say that the reachability condition s ->* t is *feasible* if there is a substitution \sigma instantiating the variables in s and t such that ...
  • thumb
    Innermost Termination of Context-Sensitive Rewriting 
    Alarcón Jiménez, Beatriz (Universitat Politècnica de València, 2011-11-28)
    Innermost context-sensitive rewriting (CSR) has been proved useful for modeling the computational behavior of programs of algebraic languages like Maude. We adapt the Dependency Pairs Framework to innermost CSR since, up ...
  • thumb
    Local confluence of conditional and generalized term rewriting systems 
    Lucas Alba, Salvador (Elsevier, 2024-01)
    [EN] Reduction-based systems are used as a basis for the implementation of programming languages, automated reasoning systems, mathematical analysis tools, etc. In such inherently non deterministic systems, guaranteeing ...