Buscar en RiuNet

Listar

Todo RiuNet

Mi cuenta

Acceder

Ayuda RiuNet

Admin. UPV

Listar por palabra clave "Maude"

Mostrando ítems 1-20 de 39

Página siguiente

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 ...
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, ...
An Efficient Canonical Narrowing Implementation with Irreducibility and SMT Constraints for Generic Symbolic Protocol Analysis

López-Rueda, Raúl; Escobar Román, Santiago; Sapiña-Sanchis, Julia (Elsevier, 2023-10)

[EN] Narrowing and unification are very useful tools for symbolic analysis of rewrite theories, and thus for any model that can be specified in that way. A very clear example of their application is the field of formal ...
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 ...
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, ...
Automation of Timed Processes in Maude-NPA using Maude

Aldama Medina, Claudia Daniela (Universitat Politècnica de València, 2021-10-07)

[ES] El desarrollo de este trabajo fin de grado tiene como objetivo automatizar el modelado de un protocolo con tiempo real en Maude-NPA. Se define una sintaxis nueva para procesos con tiempo junto con transformaciones ...
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 ...
Diseño y Desarrollo de una Técnica y Sistema de Especialización Incremental en Maude

Galán Pascual, Daniel (Universitat Politècnica de València, 2021-09-15)

[ES] El estado del arte en el diseño de herramientas de especialización automática de código está enfocado a la construcción de herramientas monolíticas, donde se priman la automatización completa y la eficiencia frente a ...
Diseño, modelado y verificación de un protocolo nuevo de autenticación usando Maude

Gallifa Tronch, Enrique (Universitat Politècnica de València, 2024-09-06)

[ES] El objetivo de este trabajo fin de máster consiste en diseñar un nuevo protocolo de autenticación en colaboración con una empresa de la comunidad valenciana y realizar el modelado y verificación de propiedades de ...
Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME system

Alpuente Frasnedo, María; Ballis, D.; Sapiña-Sanchis, Julia (Springer, 2020-09)

[EN] Program specialization is mainly recognized as a powerful technique for optimizing software systems. Nonetheless, it can also be productively employed in other application areas. This paper presents an assertion-guided ...
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 ...
Formal Analysis of Reddit Network Interactions

Padró Ferragut, Cristina (Universitat Politècnica de València, 2021-09-14)

[EN] With the rise in popularity of social media platforms in the last couple of decades, there is a demand for a more thorough and formal understanding of how these networks operate due to how quickly information is ...
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 ...
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 ...
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, ...
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 ...
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 ...
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 ...
Modelado y verificación del mecanismo de encapsulación de claves post-cuánticas KYBER usando Maude

García Valero, Víctor (Universitat Politècnica de València, 2022-09-23)

[ES] Las tecnologías de la información y la comunicación dan forma a los sistemas del mundo de hoy, y esos sistemas dan forma a la sociedad en la que vivimos. La seguridad de esos sistemas se basa en problemas matemáticos ...
Modelado y verificación del protocolo de exclusión mutua con tiempo real Fischer usando Maude

García Valero, Víctor (Universitat Politècnica de València, 2021-09-15)

[ES] En el siguiente trabajo modelamos el protocolo de exclusión mutua con tiempo real Fischer como un módulo de sistema mediante el lenguaje de especificación y verificación Maude. Hacemos uso del alcance de la generación ...