Autor:
Gutiérrez, Raúl

Foto de perfil
E-mails conocidos
r.gutierrez@upm.es
rgutierrez@dsic.upv.es
rgutierrez11@gmail.com
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Gutiérrez
Nombre de pila
Raúl
Nombre
Nombres alternativos
Afiliaciones conocidas
DSIC, Universitat Politècnica de València, Spain
Universidad Politécnica de Madrid, Spain
Universitat Politècnica de València, Spain
Páginas web conocidas
http://www.dsic.upv.es/~rgutierrez
Página completa del ítem
Notificar un error en este autor

Filtros

2016 - 201922020 - 20211
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 3 de 3
  • Miniatura
    Artículo
    A tool for the automatic generation of logical models of order-sorted first-order theories
    Gutié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.
  • Miniatura
    Artículo
    An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA
    Aparicio Sanchez, Damian; Escobar, Santiago; Gutiérrez, Raúl; Sapiña, Julia. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    Publicado en 25th European Symposium on Research in Computer Security (ESORICS 2020).
  • Miniatura
    Artículo
    infChecker: A Tool for Checking Infeasibility
    Gutié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.