- -

Browsing by Subject "Maude"

RiuNet: Institutional repository of the Polithecnic University of Valencia

Browsing by Subject "Maude"

Sort by: Order: Results:

  • thumb
    A conditional slicing tool for Maude 
    Sapiña Sanchis, Julia (Universitat Politècnica de València, 2012-10-02)
    In this work we develop Julienne, an online trace slicer for the high performance rewriting logic language Maude. Trace slicing is a widely used technique for execution trace analysis that is effectively used in program ...
  • thumb
    A Rewriting-based, Parameterized Exploration Scheme for the Dynamic Analysis of Complex Software Systems 
    Frechina Navarro, Francisco (Universitat Politècnica de València, 2014-11-17)
    Los sistemas software actuales son artefactos complejos cuyo comportamiento es a menudo extremadamente difícil de entender. Este hecho ha llevado al desarrollo de metodologías formales muy sofisticadas para el análisis, ...
  • Icon
    Análisis simbólico de planes de evolución para líneas de producto software 
    Cerveró Gregori, Pere (Universitat Politècnica de València, 2021-01-21)
    [ES] El objetivo de este trabajo es desarrollar una técnica de análisis simbólico para planes de evolución de líneas de producto software, una colección de productos estrechamente relacionados que satisfacen las necesidades ...
  • thumb
    Assertion-based Analysis via Slicing with ABETS 
    Alpuente Frasnedo, María; Frechina, F.; Sapiña Sanchis, Julia; Ballis, Demis (Cambridge University Press (CUP), 2016-09)
    [EN] We present ABETS, an assertion-based, dynamic analyzer that helps diagnose errors in Maude programs. ABETS uses slicing to automatically create reduced versions of both a run's execution trace and executed program, ...
  • thumb
    Debugging Maude programs via runtime assertion checking and trace slicing 
    Alpuente Frasnedo, María; Ballis, Demis; Frechina, F.; Sapiña-Sanchis, Julia (Elsevier, 2016-08)
    In this paper we propose a dynamic analysis methodology for improving the diagnosis of erroneous Maude programs. The key idea is to combine runtime checking and dynamic trace slicing for automatically catching errors at ...
  • thumb
    Exploring Conditional Rewriting Logic Computations 
    Alpuente Frasnedo, María; Ballis, Demis; Frechina Navarro, Francisco; Sapiña Sanchis, Julia (Elsevier, 2015)
    [EN] Trace exploration is concerned with techniques that allow computation traces to be dynamically searched for specific contents. Depending on whether the exploration is carried backward or forward, trace exploration ...
  • thumb
    Formal Modeling of Security Policies for Mobile Access Solutions 
    Roselló Gil, Guillermo (Universitat Politècnica de València, 2017-10-30)
    [EN] Current technology allows us to have a great deal of computation power in the palm of our hand in the form of smartphones. Such powerful and versatile devices are the perfect tools to, e.g., authenticate users in ...
  • thumb
    Implementación de un lenguaje de definición de operaciones complejas en Gestión de Modelos para la herramienta MOMENT 
    Gómez Llana, Abel (Universitat Politècnica de València, 2011-11-02)
    La Ingeniería dirigida por Modelos permite incrementar la productividad en el proceso de desarrollo software, obteniendo herramientas más interoperables y sencillas de mantener mediante técnicas que elevan el nivel de ...
  • thumb
    Imposing Assertions in Maude via Program Transformation 
    Alpuente Frasnedo, María; Ballis, Demis; Sapiña-Sanchis, Julia (Elsevier, 2019)
    [EN] Program transformation is widely used for producing correct mutations of a given program so as to satisfy the user's intent that can be expressed by means of some sort of specification (e.g. logical assertions, ...
  • thumb
    Inspecting Maude Variants with GLINTS 
    Alpuente Frasnedo, María; Cuenca-Ortega, Angel; Escobar Román, Santiago; Sapiña-Sanchis, Julia (Cambridge University Press, 2017)
    [EN] This paper introduces GLINTS, a graphical tool for exploring variant narrowing computations in Maude. The most recent version of Maude, version 2.7.1, provides quite sophisticated unification features, including ...
  • thumb
    Logic-based techniques for program analysis and specification synthesis 
    Feliú Gabaldón, Marco Antonio (Universitat Politècnica de València, 2013-11-19)
    La Tesis investiga técnicas ágiles dentro del paradigma declarativo para dar solución a dos problemas: el análisis de programas y la inferencia de especificaciones a partir de programas escritos en lenguajes multiparadigma ...
  • thumb
    Modelado y verificación de programas Event-B usando Maude 
    Ruiz Pérez, Francisca de Asís (Universitat Politècnica de València, 2016-05-13)
    [ES] La mayoría de herramientas de modelado en Ingeniería del Software carecen de mecanismos de verificación de propiedades basados en métodos formales, aunque existen muchas alternativas que incluyen métodos formales ...
  • thumb
    Normal forms and normal theories in conditional rewriting 
    Lucas Alba, Salvador; Meseguer, Jose (Elsevier, 2016-01)
    We present several new concepts and results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs), which support types, subtypes and rewriting modulo axioms, and contains the ...
  • thumb
    Order-Sorted Equality Enrichments Modulo Axioms 
    Gutiérrez Gil, Raúl; Meseguer, Jose; Rocha, Camilo (Elsevier, 2015-03-07)
    Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications ...
  • thumb
    Order-sorted Homeomorphic Embedding modulo Combinations of Associativity and/or Commutativity Axioms 
    Alpuente Frasnedo, María; Cuenca-Ortega, Angel; Escobar Román, Santiago; Meseguer, José (IOS Press, 2020)
    [EN] The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been ...
  • thumb
    Partial Evaluation of Rewriting Logic Theories 
    Cuenca Ortega, Ángel Eduardo (Universitat Politècnica de València, 2019-11-04)
    [ES] La evaluación parcial de programas es una técnica general y potente de optimización de programas que preserva su semántica y tiene muchas aplicaciones relevantes. La optimización se consigue al especializar programas ...
  • thumb
    Protocol analysis modulo exclusive-or theories: a case study in Maude-MPA 
    González Burgueño, Antonio (Universitat Politècnica de València, 2015-06-16)
    [EN] Escobar of the Universitat Politècnica de València in collaboration with José Meseguer (University of Illinois at Urbana-Champaign, USA) and Catherine Meadows (Naval Research Lab, Washington, DC, USA). We focus on ...
  • thumb
    Rewriting Logic Techniques for Program Analysis and Optimization 
    Sapiña Sanchis, Julia (Universitat Politècnica de València, 2018-01-08)
    Esta tesis propone una metodología de análisis dinámico que mejora el diagnóstico de programas erróneos escritos en el lenguaje Maude. La idea clave es combinar técnicas de verificación de aserciones en tiempo de ejecución ...
  • Icon
    Static correction of Maude programs with assertions 
    Alpuente Frasnedo, María; Ballis, D.; Sapiña-Sanchis, Julia (Elsevier, 2019-07)
    [Otros] In this paper, we present a novel transformation method for Maude programs featuring both automatic program diagnosis and correction. The input of our method is a reference specification of the program behavior ...
  • thumb
    Static Correction of Maude Programs with Assertions 
    Alpuente Frasnedo, María; Ballis, D.; Sapiña Sanchis, Julia (Universitat Politècnica de València, 2018-04-12)
    In this paper, we present a novel transformation method for Maude programs featuring both automatic program diagnosis and correction. The input of our method is a reference specification A of the program behavior that ...