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 ...
[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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
[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 ...
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 ...
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 ...
[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 ...
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 ...
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 ...
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 ...
[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 ...
Reinoso Mendoza, Efren Patricio(Universitat Politècnica de València, 2016-12-07)
[EN]
In Computer Science and Software Engineering, even at this time, when huge hardware and software resources are available, the problem of checking correctness of an speciﬁc piece of software is a very complicated one. ...