- -

Listar por palabra clave "Program analysis"

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

Listar por palabra clave "Program analysis"

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
    A Framework for Computing Finite SLD Trees 
    Nishid, Naoki; Vidal Oriola, Germán Francisco (Elsevier, 2015-03)
    The search space of SLD resolution, usually represented by means of a so-called SLD tree, is often infinite. However, there are many applications that must deal with possibly infinite SLD trees, like partial evaluation or ...
  • thumb
    Analysis Techniques for Software Maintenance 
    Pérez Rubio, Sergio (Universitat Politècnica de València, 2023-05-05)
    [ES] Vivimos en una sociedad donde la digitalización está presente en nuestro día a día. Nos despertamos con la alarma de nuestro teléfono móvil, apuntamos nuestras reuniones en nuestro calendario digital, guardamos nuestros ...
  • thumb
    Annotation of logic programs for independent AND-Parallelism by partial evaluation 
    Vidal Oriola, Germán Francisco (Cambridge University Press (CUP), 2012-07)
    Traditional approaches to automatic AND-parallelization of logic programs rely on some static analysis to identify independent goals that can be safely and efficiently run in parallel in any possible execution. In this ...
  • 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 ...
  • 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
    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
    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
    MU-TERM: Verify Termination Properties Automatically (System Description) 
    Gutiérrez Gil, Raúl; Lucas Alba, Salvador (Springer Nature, 2020-07-06)
    [EN] We report on the new version of mu-term, a tool for proving termination properties of variants of rewrite systems, including conditional, context-sensitive, equational, and order-sorted rewrite systems. We follow a ...
  • Icon
    Program Slicing for Modern Programming Languages 
    Galindo Jiménez, Carlos Santiago (Universitat Politècnica de València, 2025-09-24)
    [ES] Producir software eficiente y efectivo es una tarea que parece ser tan difícil ahora como lo era para los primeros ordenadores. Con cada mejora de hardware y herramientas de desarrollo (como son compiladores y ...
  • thumb
    Proving and disproving confluence of context-sensitive rewriting 
    Lucas Alba, Salvador; Vítores-Vicente, Miguel; Gutiérrez Gil, Raúl (Elsevier, 2022-04)
    [EN] Context-sensitive rewriting is a restriction of term rewriting where reductions are allowed on specific arguments of function symbols only, and then in particular positions of terms. Confluence is an abstract property ...
  • Icon
    Proving Confluence in the Confluence Framework with CONFident 
    Gutiérrez, Raúl; Lucas Alba, Salvador; Vítores-Vicente, Miguel (IOS Press, 2024)
    [EN] This article describes the confluence framework, , a novel framework for proving disproving confluence using a divide-and-conquer modular strategy, and its implementation CONFident. . Using this approach, we are able ...
  • thumb
    Proving Termination of Context-Sensitive Rewriting with MU-TERM 
    Alarcón, Beatriz; Gutiérrez Gil, Raúl; Iborra, José; Lucas Alba, Salvador (Elsevier, 2007-07-16)
    [EN] Context-sensitive rewriting (CSR) is a restriction of rewriting which forbids reductions on selected arguments of functions. Proving termination of CSR is an interesting problem with several applications in the fields ...
  • thumb
    Reducing relative termination to dependency pair problems 
    Iborra, José; Nishida, Naoki; Vidal Oriola, Germán Francisco; Yamada, Akihisa (Springer, 2015-07-25)
    Relative termination, a generalized notion of termination, has been used in a number of different contexts like proving the confluence of rewrite systems or analyzing the termination of narrowing. In this paper, we introduce ...
  • thumb
    Slicing unconditional jumps with unnecessary control dependencies 
    Galindo-Jiménez, Carlos Santiago; Pérez-Rubio, Sergio; Silva, Josep (Springer-Verlag, 2021-02-13)
    [EN] Program slicing is an analysis technique that has a wide range of applications, ranging from compilers to clone detection software, and that has been applied to practically all programming languages. Most program ...