[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, ...
[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, ...
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 ...
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 ...
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 ...
[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 ...
[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 ...
[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, ...
Trace inspection is concerned with techniques that allow the
trace content to be searched for specific components. This paper presents
a rich and highly dynamic, parameterized technique for the trace inspection
of ...
Alpuente Frasnedo, María; Ballis, Demis; Escobar Román, Santiago; Sapiña Sanchis, Julia(Universitat Politècnica de València, 2020-06-08)
Partial evaluation has been never investigated in the context of rewrite theories that allow concurrent systems to be specified by means of rules, with an underlying equational theory being used to model system states as ...
Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we investigate the semantic properties of a narrowing-based ...
[EN] In this paper, we develop an automated optimization framework for rewrite theories that supports sorts, subsort overloading, equations and algebraic axioms with free/nonfree constructors, and rewrite rules modeling ...
Sapiña Sanchis, Julia(Universitat Politècnica de València, 2018-01-08)
Esta tesis propone una metodología de análisis dinámico que mejora el diagnóstico de programas erróneos escritos en el lenguaje Maude. La idea clave es combinar técnicas de verificación de aserciones en tiempo de ejecución ...
[EN] Keeping XML data in a consistent state w.r.t. both structure and content is a burdensome
task. To maintain the consistency of ever-larger, complex XML repositories,
suitable mechanisms that are able to x every ...
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 ...
Ballis, Demis(Universitat Politècnica de València, 2008-05-07)
The increasing complexity of software systems has led to the development of sophisticated formal Methodologies for verifying and correcting data and programs. In general, establishing whether a program behaves correctly ...