Person:
Albert Albiol, Elvira María

First Name

Elvira María

Last Name

Albert Albiol

URI

https://hdl.handle.net/20.500.14352/78699

Affiliation

Universidad Complutense de Madrid

Faculty / Institute

Informática

Department

Sistemas Informáticos y Computación

Area

Lenguajes y Sistemas Informáticos

Identifiers

Full item page

Search Results

Now showing 1 - 10 of 40

Project number: 198
Diseño de una metodología para la implantación de herramientas automáticas de corrección de estilo y buenas prácticas en asignaturas de programación
(2017) Correas Fernández, Jesús; Román Díez, Guillermo; Albert Albiol, Elvira María; Arenas Sánchez, Purificación; Genaim, Samir; Gómez-Zamalloa Gil, Miguel
Project number: PIMCD43/23-24
Estudio de la aplicación de herramientas de análisis de contratos inteligentes de Ethereum en las asignaturas de blockchain de las titulaciones de la Facultad de Informática
(2024) Gordillo Alguacil, Pablo; Albert Albiol, Elvira María; Correas Fernández, Jesús; Genaim, Samir; Isabel Márquez, Miguel; Román Díez, Guillermo; Rubio Gimeno, Alberto
Conditional Termination of Loops over Heap-Allocated Data
(Science of computer programming, 2014) Albert Albiol, Elvira María; Arenas Sánchez, Purificación; Genaim, Samir; Puebla, Germán; Román Díez, Guillermo
Static analysis which takes into account the values of data stored in the heap is considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields nor of array contents, i.e., they are heap-insensitive. In this article, we propose locality conditions for soundly tracking heap-allocated data in Java (bytecode) programs, by means of ghost non-heap allocated variables. This way, heap-insensitive analysis over the transformed program can infer information on the original heap-allocated data without sacrificing efficiency. If the locality conditions cannot be proven unconditionally, we seek to generate aliasing preconditions which, when they hold in the initial state, guarantee the termination of the program. Experimental results show that we greatly improve the accuracy w.r.t. a heap-insensitive analysis while the overhead introduced is reasonable.
Project number: 245
Desarrollo de una herramienta de depuración simbólica para las asignaturas de iniciación a la programación en las facultades de Informática y Estudios Estadísticos
(2015) Gómez-Zamalloa Gil, Miguel; Albert Albiol, Elvira María; Arenas Sánchez, Purificación; Correas Fernández, Jesús; Genaim, Samir; Puebla Sánchez, Germán; Román Díez, Guillermo; Peces, Raquel; Giraldo, Carlos Gabriel; Antolín, Clara
El proyecto plantea el desarrollo de una herramienta de depuración simbólica que ayude a los estudiantes de las asignaturas de iniciación a la programación en las facultades de Informática y Estudios Estadísticos
Project number: 281
Aplicación del sistema jPET para la generación automática de tests en asignaturas de programación con Java
(2016) Gómez-Zamalloa Gil, Miguel; Albert Albiol, Elvira María; Arenas Sánchez, Purificación; Correas Fernández, Jesús; Genaim, Samir; Román Díez, Guillermo
Parallel Cost Analysis of Distributed Systems
(2015) Albert Albiol, Elvira María; Correas Fernández, Jesús; Johnsen, Einar Broch; Román Díez, Guillermo
We present a novel static analysis to infer the parallel cost of distributed systems. Parallel cost differs from the standard notion of serial cost by exploiting the truly concurrent execution model of distributed processing to capture the cost of synchronized tasks executing in parallel. It is challenging to analyze parallel cost because one needs to soundly infer the parallelism between tasks while accounting for waiting and idle processor times at the different locations. Our analysis works in three phases: (1) It first performs a block-level analysis to estimate the serial costs of the blocks between synchronization points in the program; (2) Next, it constructs a distributed ow graph (DFG) to capture the parallelism, the waiting and idle times at the locations of the distributed system; Finally, (3) the parallel cost can be obtained as the path of maximal cost in the DFG. A prototype implementation demonstrates the accuracy and feasibility of the proposed analysis.
Peak Cost Analysis of Distributed Systems (Author's version)
(2014) Albert Albiol, Elvira María; Correas Fernández, Jesús; Román Díez, Guillermo
We present a novel static analysis to infer the peak cost of distributed systems. The different locations of a distributed system communicate and coordinate their actions by posting tasks among them. Thus, the amount of work that each location has to perform can greatly vary along the execution depending on: (1) the amount of tasks posted to its queue, (2) their respective costs, and (3) the fact that they may be posted in parallel and thus be pending to execute simultaneously. The peak cost of a distributed location refers to the maximum cost that it needs to carry out along its execution. Inferring the peak cost is challenging because it increases and decreases along the execution, unlike the standard notion of total cost which is cumulative. Our key contribution is the novel notion of quantified queue configuration which captures the worst-case cost of the tasks that may be simultaneously pending to execute at each location along the execution. A prototype implementation demonstrates the accuracy and feasibility of the proposed peak cost analysis.
Non-Cumulative Resource Analysis (Author’s version)
(Lecture notes in computer science, 2015) Albert Albiol, Elvira María; Correas Fernández, Jesús; Román Díez, Guillermo
Existing cost analysis frameworks have been defined for cumulative resources which keep on increasing along the computation. Traditional cumulative resources are execution time, number of executed steps, amount of memory allocated, and energy consumption. Noncumulative resources are acquired and (possibly) released along the execution. Examples of non-cumulative cost are memory usage in the presence of garbage collection, number of connections established that are later closed, or resources requested to a virtual host which are released after using them. We present, to the best of our knowledge, the first generic static analysis framework to infer an upper bound on the peak cost for non-cumulative types of resources. Our analysis comprises several components: (1) a pre-analysis to infer when resources are being used simultaneously, (2) a program-point resource analysis which infers an upper bound on the cost at the points of interest (namely the points where resources are acquired) and (3) the elimination from the upper bounds obtained in (2) of those resources accumulated that are not used simultaneously. We report on a prototype implementation of our analysis that can be used on a simple imperative language.
Quantified Abstract Configurations of Distributed Systems
(Formal Aspects of Computing, 2014) Albert Albiol, Elvira María; Correas Fernández, Jesús; Puebla, Germán; Román Díez, Guillermo
When reasoning about distributed systems, it is essential to have information about the different kinds of nodes that compose the system, how many instances of each kind exist, and how nodes communicate with other nodes. In this paper we present a static-analysis-based approach which is able to provide information about the questions above. In order to cope with an unbounded number of nodes and an unbounded number of calls among them, the analysis performs an abstraction of the system producing a graph whose nodes may represent (infinitely) many concrete nodes and arcs represent any number of (infinitely) many calls among nodes. The crux of our approach is that the abstraction is enriched with upper bounds inferred by resource analysis that limit the number of concrete instances that the nodes and arcs represent and their resource consumption. The information available in our quantified abstract configurations allows us to define performance indicators which measure the quality of the system. In particular, we present several indicators that assess the level of distribution in the system, the amount of communication among distributed nodes that it requires, and how balanced the load of the distributed nodes that compose the system is. Our performance indicators are given as functions on the input data sizes, and they can be used to automate the comparison of different distributed settings and guide towards finding the optimal configuration.
Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-based Instance, and Actor-based Concurrency
(2014) Albert Albiol, Elvira María; Arenas Sánchez, Purificación; Gómez Zamalloa, Miguel; Rojas, José Miguel
The focus of this tutorial is white-box test case generation (TCG) based on symbolic execution. Symbolic execution consists in executing a program with the contents of its input arguments being symbolic variables rather than concrete values. A symbolic execution tree characterizes the set of execution paths explored during the symbolic execution of a program. Test cases can be then obtained from the successful branches of the tree. The tutorial is split into three parts: (1) The first part overviews the basic techniques used in TCG to ensure termination, handling heap-manipulating programs, achieving compositionality in the process and guiding TCG towards interesting test cases. (2) In the second part, we focus on a particular implementation of the TCG framework in constraint logic programming (CLP). In essense, the imperative object-oriented program under test is automatically transformed into an equivalent executable CLP-translated program. The main advantage of CLP-based TCG is that the standard mechanism of CLP performs symbolic execution for free. The PET system is an open-source software that implements this approach. (3) Finally, in the last part, we study the extension of TCG to actor-based concurrent programs.