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 ...
Generalization, also called anti-unification, is the dual of unification. Given terms t and t
,
a generalizer is a term t of which t and t are substitution instances. The dual of
a most general unifier (mgu) is that of ...
[EN] Partial evaluation is a powerful and general program optimization technique with many successful applications. Existing PE schemes do not apply to expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ...
[EN] Partial evaluation (PE) is a branch of computer science that achieves code optimization via specialization. This article describes a PE methodology for optimizing rewrite theories that encode concurrent as well as ...
Alpuente Frasnedo, María; Ballis, Demis; Romero, Daniel Omar(Elsevier, 2014-02-15)
[EN] This paper develops a Rewriting Logic framework for the automatic specification and verification of Web applications that considers the critical aspects of concurrent Web interactions, browser navigation features ...
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, ...
Alba Castro, Mauricio Fernando(Universitat Politècnica de València, 2011-11-28)
In this thesis we propose an abstraction based certification technique for Java programs which is based on rewriting logic, a very general logical and semantic framework efficiently implemented in the functional programming ...
Alpuente Frasnedo, María; Pardo Pont, Daniel; Villanueva García, Alicia(Universitat Politècnica de València, 2018-04-12)
[EN] In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based ...
[EN] In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KERNELC, that supports pointer-based ...
Computing generalizers is relevant in a wide spectrum of automated
reasoning areas where analogical reasoning and inductive inference
are needed. The ACUOS system computes a complete and minimal
set of semantic generalizers ...
Espert Real, Javier(Universitat Politècnica de València, 2013-02-06)
[ES] La generalización, también denominada anti-unificación, es la operación dual de la unificación. Dados dos términos t y t' , un generalizador es un término t'' del cual t y t' son instancias de sustitución. El concepto ...
Vidal Oriola, Germán Francisco(Universitat Politècnica de València, 2015-10-08)
El problema de la integraci on de la programaci on l ogica y funcional est a considerado
como uno de los m as importantes en el area de investigaci on sobre programaci on
declarativa. Para que los lenguajes declarativos ...
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 ...
[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, ...
[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 ...
Alpuente Frasnedo, María; Feliú Gabaldón, Marco Antonio; Villanueva García, Alicia(Association for Computing Machinery (ACM), 2013-01-21)
Formal specifications can be used for various software engineering activities ranging from finding errors to documenting software and automatic test-case generation. Automatically discovering specifications for heap-manipulating ...
Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. In this paper, we present a backward trace slicing technique that can be used ...
Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. In this paper, we present a backward trace slicing technique that can be used ...
Alba Castro, Mauricio Fernando(Universitat Politècnica de València, 2011-10-20)
En esta tesis se presenta una metodología y la implementación correspondiente para la certificación de propiedades de seguridad de programas Java, basada en lógica de reescritura, semántica de lenguajes de programación e ...