Búsqueda avanzada

El autor Adrián Riesco ha publicado 4 artículo(s):

1 - Towards a Formal Semantics-Based Technique for Interprocedural Slicing

Interprocedural slicing is a technique applied on programs with procedures which relies on how the information is passed at procedure call/return sites. Such a technique computes program slices (i.e. program fragments restricted w.r.t. a given criterion). The existing approaches to interprocedural slicing exploit the particularities of the underlying language semantics in order to compute program slices. In this paper we propose a generic technique for interprocedural slicing. More specifically, our approach works with inferred particularities of a language semantics, given as a rewriting-logic specification, and computes program slices using a term slicing-based algorithm.

Autores: Irina Mariuca Asavoae / Mihail Asavoae / Adrian Riesco / 
Palabras Clave:

2 - EDD: A Declarative Debugger for Sequential Erlang Programs (High-level Work)

Declarative debuggers are semi-automatic debugging tools that abstract the execution details to focuson the program semantics. This paper presents a tool implementing this approach for the sequentialsubset of Erlang, a functional language with dynamic typing and strict evaluation. Given an erro-neous computation, it first detects an erroneous function (either a «named» function or a lambda-abstraction), and then continues the process to identify the fragment of the function responsible forthe error. Among its features it includes support for exceptions, predefined and built-in functions,higher-order functions, and trusting and undo commands.

Autores: Rafael Caballero / Enrique Martin-Martin / Adrián Riesco / 
Palabras Clave:

3 - Using Big-step and Small-step Semantics to Perform Declarative Debugging (High-level Work)

Declarative debugging is a semi-automatic debugging technique that abstracts the execution details to focus on results. This technique builds a debugging tree representing an incorrect computation and traverses it by asking questions to the user until the error is found. In previous works we have presented a declarative debugger for Maude specifications. Besides a programming language, Maude is a semantic framework where several other languages can be specified. However, our declarative debugger is only able to find errors in Maude specifications, so it cannot find bugs on the programs written on the languages being specified. We study in this paper how to modify our declarative debugger to find this kind of errors when defining programming languages using big-step and smallstep semantics, two generic approaches that allow to specify a wide range of languages in a natural way. We obtain our debugging trees by modifying the proof trees obtained from the semantic rules. We have extended our declarative debugger to deal with this kind of debugging, and examples have been developed to test its feasibility.

Autores: Adrián Riesco / 
Palabras Clave:

4 - Towards a formal framework for analyzing stream processing systems in Maude (Trabajo en progreso)

With the rise of Big Data technologies, distributed stream processing systems (SPS) have gained popularity in the last years. Among these systems Spark Streaming stands out as a particularly attractive option, with a growing adoption in the industry, so we will consider in particular some features of SPS in Spark Streaming. Maude is a high-performance logical framework where other systems can be easily specified and executed. In this paper we show how a Maude specification of Spark Streaming would allow developers to analyze and prove properties on their programs.

Autores: Adrián Riesco / Miguel Palomino / Narciso Martí-Oliet / 
Palabras Clave: Maude - Model checking - Stream processing systems