This paper introduces the idea of using assertion checking for enhancing the dynamic slicing of Maude computation traces. Since trace slicing can greatly simplify the size and complexity of the analyzed traces, our methodology ...
Orengo Faus, Sandra María(Universitat Politècnica de València, 2022-10-21)
[ES] En Ingeniería de Software, el concepto de contrato está relacionado con una especificación del comportamiento de los programas utilizando descripciones que típicamente incluyen precondiciones y postcondiciones. El ...
Coroban, Raul Ionut(Universitat Politècnica de València, 2018-09-11)
[EN] In Software Engineering, software contracts allow the program behavior to be specified
using formal axioms such as preconditions, postconditions and invariants. The current
state of the art makes it possible to ...
Alpuente Frasnedo, María; Feliú Gabaldón, Marco Antonio; Joubert, Christophe; Villanueva García, Alicia(Springer Verlag (Germany), 2011)
This paper describes two techniques for Datalog query evaluation and their application to object-oriented program analysis. The first technique transforms Datalog programs into an implicit Boolean Equation System (Bes) ...
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 ...
[EN] Web-TLR is a Web verification engine that is based on the well-established Rewriting Logic--Maude/LTLR tandem for Web system specification and model-checking. In Web-TLR, Web applications are expressed as rewrite ...
Rubio Salvador, Sergio(Universitat Politècnica de València, 2019-09-19)
[ES] El objetivo de este trabajo es realizar la migración de una aplicación de gestión de
partes en movilidad para una compañía que provee servicios globales esenciales,
incluido el sector de las telecomunicaciones. A ...
Requena Casares, Cristina(Universitat Politècnica de València, 2016-09-30)
[ES] El concepto de aplicación web está relacionado con el almacenamiento en la nube
y el acceso a la información vía Internet, quedando una copia temporal dentro de
nuestro dispositivo. Sin embargo, las aplicaciones web ...
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 ...
[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 ...
Feliú Gabaldón, Marco Antonio(Universitat Politècnica de València, 2011-12-15)
Two approaches for evaluating Datalog programs are presented: one based on boolean
equation systems, and the other based on rewriting logic. The work is presented in the
context of the static analysis of Java programs ...
[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 ...
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 ...
[EN] This special issue contains improved versions of selected papers from the workshops
on Formal Methods for Industrial Critical Systems (FMICS) held in Eindhoven,
The Netherlands, in November 2009 and in Antwerp, ...
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 ...
[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, ...
Pardo Pont, Daniel(Universitat Politècnica de València, 2016-07-20)
[EN] Despite its many unquestionable benefits, formal specifications are not widely used in industrial software development. In order to reduce the time and effort required to write formal specifications, in this Master ...
[EN] Despite its many unquestionable benefits, formal specifications are not widely used in industrial software development. In order to reduce the time and effort required to write formal specifications, in this paper we ...
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 ...