Buscar en RiuNet

Listar

Todo RiuNet

Mi cuenta

Acceder

Ayuda RiuNet

Admin. UPV

Listar por palabra clave "Rewriting logic"

Mostrando ítems 1-20 de 23

Página siguiente

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, ...
Backward Trace Slicing for Rewriting Logic Theories -Technical report -

Alpuente Frasnedo, María; Ballis, D.; Espert, J.; Romero, D. (Universitat Politècnica de València, 2011-04-19)

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 ...
Datalog-Based program analysis with BES and RWL

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) ...
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 ...
Evaluation of Datalog queries and its application to the static analysis of Java code

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 ...
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 ...
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, ...
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 ...
Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude

García, Víctor; Escobar Román, Santiago; Ogata, Kazuhiro (Sun SITE Central Europe, 2022)

[EN] Communication and information technologies shape the world¿s systems of today, and those systems shape the society we live in. The security of those systems relay on mathematical problems hard to solve for classical ...
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 ...
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 ...
Regression Test-Driven Extension of PLEXIL5: Support for Update Nodes

Moreno Latorre, Jorge (Universitat Politècnica de València, 2023-09-26)

[EN] This project describes the extension effort of PLEXIL5, a PLEXIL formal interpreter specified in the rewriting logic engine Maude, to achieve higher degrees of correctness and completeness with respect to the PLEXIL ...
Rewriting-based Verification and Debugging of Web Systems

Romero ., Daniel Omar (Universitat Politècnica de València, 2011-11-02)

The increasing complexity of Web system has led to the development of sophisticated formal methodologies for verifying and correcting Web data and Web programs. In general, establishing whether a Web system behaves ...
Safety enforcement via programmable strategies in Maude

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

[ES] El objetivo de este trabajo es formalizar un mecanismo general para garantizar la seguridad de las computaciones en lógica de reescritura. La técnica propuesta consiste en una transformación de programas que garantiza ...
Slicing slices, an incremental backward trace slicing methodology for rwl computations

Sapiña Sanchis, Julia (Universitat Politècnica de València, 2014-11-28)

[EN] Execution traces are an important source of information for program understanding and debugging. However, they have as an important drawback that they are commonly huge and complex, making their manual analysis ...
Slicing-based debugging of web applications in rewriting logic

Frechina Navarro, Francisco (Universitat Politècnica de València, 2012-05-14)

The pervasiveness of computing on the Internet has led to an explosive growth of Web applications that, together with their ever-increasing complexity, have turned their design and development in a major challenge. Un ...
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 ...
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 ...
Strong and weak operational termination of order-sorted rewrite theories

Lucas Alba, Salvador; Meseguer, José (Springer Verlag (Germany), 2014-11)

This paper presents several new results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs) which contains the more restricted framework of conditional term rewriting systems ...
Symbolic Analysis of Maude Theories with Narval

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 ...