We present iJulienne, a trace analyzer for conditional rewriting
logic theories that can be used to compute abstract views of Maude
executions that help users understand and debug programs. Given a
Maude execution trace ...
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 ...
[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 ...
Padró Ferragut, Cristina(Universitat Politècnica de València, 2022-10-11)
[ES] Se prevé que los vehículos sean completamente autónomos para 2040, lo que previsiblemente aportará beneficios considerables a la sociedad. Los vehículos autónomos (AV) dependen en gran medida de los avances en muchas ...
Alpuente Frasnedo, María; Escobar Román, Santiago; Sapiña-Sanchis, Julia; Ballis, Demis(Cambridge University Press, 2019-09)
[EN] Concurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic ...
Alpuente Frasnedo, María; Escobar Román, Santiago; Ballis, Demis; Sapiña-Sanchis, Julia(Cambridge University Press, 2022-05)
[EN] This paper introduces Presto, a symbolic partial evaluator for Maude's rewriting logic theories that can improve system analysis and verification. In Presto, the automated optimization of a conditional rewrite theory ...
Iborra López, José(Universitat Politècnica de València, 2011-11-28)
In this work, we generalize the Dependency Pairs approach for automated proofs of termination to prove the termination of narrowing.We identify the phenomenon of echoing in infinite narrowing derivations and demonstrate ...
Iborra López, José(Universitat Politècnica de València, 2013-02-11)
En 1936 Alan Turing demostro que el halting problem, esto es, el problema de decidir
si un programa termina o no, es un problema indecidible para la inmensa mayoria de
los lenguajes de programacion. A pesar de ello, la ...
Ojeda Forés, Pedro(Universitat Politècnica de València, 2011-10-27)
En este trabajo se presenta, en primer lugar, una metodología de verificación y reparación de sitios Web que permite especificar requerimientos sobre el sitio Web y detectar errores en base a la especificación. Para optimizar ...
Juan Achahuanco, Arturo Raúl de(Universitat Politècnica de València, 2022-09-14)
[ES] Las herramientas de verificación de modelos model checking existentes ofrecen ciertas
facilidades para el análisis y comprensión del proceso de verificación de sistemas hardware y software. Este es el caso del ...
[EN] Understanding the behavior of software is important for the existing software to be improved. In this paper, we present a trace slicing technique that is suitable for analyzing complex, textually-large computations ...
Orengo Faus, Sandra María(Universitat Politècnica de València, 2020-10-21)
[ES] En Ingeniería de Software, el concepto de contrato está relacionado con una descripción del comportamiento de los programas utilizando precondiciones y postcondiciones de métodos. El estado del arte actual permite ...
Sanz Carreres, Sergi(Universitat Politècnica de València, 2020-09-02)
[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 ...
León Guerrero, Alejandro(Universitat Politècnica de València, 2019-09-09)
[ES] Los asistentes robóticos autónomos están diseñados para ofrecer compañía a personas que viven en un ambiente doméstico. Este tipo de robot usa diversos sensores para
detectar y adaptarse a cualquier imprevisto en el ...
Espert Real, Javier(Universitat Politècnica de València, 2011-07-20)
Web-TLR is a software tool designed for model-checking Web applications that is based on rewriting logic. Web applications are expressed as rewrite theories that can be formally verified by using the Maude built-in LTLR ...