Autor: Lucas, Salvador
Cargando...
E-mails conocidos
slucas@dsic.upv.es
http://users.dsic.upv.es/~slucas/
http://users.dsic.upv.es/~slucas/
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Lucas
Nombre de pila
Salvador
Nombre
Nombres alternativos
Afiliaciones conocidas
DSIC, Universitat Politécnica de Valéncia, Spain
Universitat Politècnica de València, Spain
Universitat Politècnica de València, Spain
Páginas web conocidas
Página completa del ítem
Notificar un error en este autor
6 resultados
Resultados de la búsqueda
Mostrando 1 - 6 de 6
Artículo Confluence of Conditional Rewriting ModuloLucas, Salvador. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.We investigate confluence of rewriting with *equational generalized rewrite systems* R, consisting of *Horn clauses*, some of them defining *conditional equations s=t <= c and *one-step reductions* l -> r <= c. In both cases, *c* is a sequence of *atoms*, possibly defined by using additional Horn clauses. Such systems include *equational term rewriting systems* and (join, oriented, and semiequational) *conditional term rewriting systems*. Equations E define the equivalence =E and quotient set T/=E of terms, where reductions s ->R/E t using rules in R occur. For such systems, we obtain a *finite* set of conditional pairs $\pi$, which can be viewed as logical sentences, to prove and disprove confluence of ->R/E by (dis)proving joinability of such conditional pairs $\pi$.Artículo Productivity of rewrite systems without transformationsLucas, Salvador. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.Termination of programs, i.e., the absence of infinite computations, ensures the existence of normal forms for all initial expressions, thus providing an essential ingredient for the definition of a normalization semantics for functional programs. In lazy functional languages, though, infinite data structures are often delivered as the outcome of computations. For instance, the list of all prime numbers can be returned as a neverending stream of numerical expressions or data structures. If such streams are allowed, requiring termination is hopeless. In this setting, the notion of productivity can be used to provide an account of computations with infinite data structures, as it “captures the idea of computability, of progress of infinite-list programs” (B.A. Sijtsma, On the Productivity of Recursive List Definitions, ACM Transactions on Programming Languages and Systems 11(4):633- 649, 1989). However, in the realm of Term Rewriting Systems, which can be seen as (first-order, untyped, unconditional) functional programs, termination of Context-Sensitive Rewriting (CSR) has been showed equivalent to productivity of rewrite systems through appropriate transformations. In this way, tools for proving termination of CSR can be used to prove productivity. In term rewriting, CSR is the restriction of rewriting that arises when reductions are allowed on selected arguments of function symbols only. In this paper we show that well-known results about the computational power or CSR are useful to better understand the existing connections between productivity of rewrite systems and termination of CSR, and also to obtain more powerful techniques to prove productivity of rewrite systems.Artículo Directions of Operational TerminationLucas, Salvador. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.A theory S in a logic supplied with an inference system is operationally terminating if no goal has an infinite well-formed proof tree. Well-formed proof trees are those which an interpreter would incrementally build when trying to solve a condition at a time from left to right. For this reason, infinite well-formed proof trees have a unique infinite branch which is called the spine. This paper introduces the notion of a directed proof tree for S and a set of formulas ?, which we call a direction. Intuitively, a direction ? is intended to collect formulas that are infinitely often used in the spine of an infinite well-formed proof tree (which is then called ?-directed) due to the repeated use of some specific inference rules. Then we introduce the notion of ?-directed operational termination of a theory as the absence of ?-directed proof trees. This new notion permits the definition of different termination properties which can be useful to distinguish different computational behaviors. It also gives a new characterization of operational termination of a (finite) theory S as the conjunction of the ?-directed operational termination of S for each direction ? in a (finite) set of directions.Artículo Automatic generation of logical models for order-sorted first-order theories in program analysisLucas, Salvador. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.Computations are often viewed as proofs of specific sentences in some computational logic describing the operational semantics of the programming language or computational system. Since the semantics of programs (i.e., the set of such specific sentences that are provable in the logic) is usually incomputable, and most program properties undecidable, abstraction is essential in program analysis. Abstractions can be formalized as semantic models which should be automatically generated in a push-the-button-and-wait style of program analysis and verification. We investigate the automatic generation of numerical models for order-sorted first-order logics and its use in program analysis. Our development systematically uses the recently introduced convex domains which are well-suited for representing domains for different sorts; we use them to interpret the ranked symbols of sorted signatures by means of appropriately adapted convex matrix interpretations. Such numerical interpretations permit the use of existing algorithms and tools from linear algebra (e.g., Farkas’ Lemma), real algebraic geometry, and arithmetic constraint solving in the implementation of the analyses.Artículo A tool for the automatic generation of logical models of order-sorted first-order theoriesGutiérrez, Raúl; Lucas, Salvador; Reinoso, Patricio. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.Semantics-based program analysis guarantees that the obtained knowledge about focused program features matches the real behaviour of the program. Automation of the analyses requires abstraction mechanisms to approximate the (usually undecidable) program semantics and targeted properties. In this setting, the logical notions of interpretation of a logic language and model of a theory provide an appropriate framework for abstraction in the sense that the corresponding analyses will be sound and, when relying on some decidable theory, amenable for automation. We describe a new tool, AGES, which is able to automatically generate models for order-sorted first-order theories. Such theories are very helpful in the semantic description of most programming languages. The current version of the tool systematically exploits (and relies on) the recently introduced convex domains which are well-suited for representing domains for different sorts; we use them to interpret the ranked symbols of order-sorted signatures and also the (also ranked) predicate symbols in the language by means of appropriately adapted convex matrix interpretations. The system is available as a web application and can be used to give support to users interested in checking properties of software modules provided that they are able to describe the property as an order-sorted first-order theory whose satisfiability guarantees the property. Examples of such properties are partial correctness, program termination, etc. The paper illustrates the use of the tool by means of simple case studies.Artículo infChecker: A Tool for Checking InfeasibilityGutiérrez, Raúl; Lucas, Salvador. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.Given a 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 the reachability test sigma(s) ->*R sigma(t) succeeds; otherwise, we call it infeasible. Given a sequence of reachability conditions (s1 = t1),...,(sn = tn), where n > 0, we say that the sequence is R-feasible if there is a substitution such that all the reachability tests sigma(si) ->*R sigma(ti) are satised. In [5, 6] we presented an approach to deal with infeasibility using a semantic criterion. In this paper we present infChecker, a new tool for checking infeasibility conditions of CTRSs based on this approach. We succesfully participated in the 2019 Confuence Competition in the INF (infeasibility) category, being the most powerful tool for checking both infeasibility and feasibility.