Person:
Genaim, Samir

First Name

Samir

Last Name

Genaim

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 10

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-02-20) Gómez-Zamalloa Gil, Miguel; Albert Albiol, Elvira; 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
Aplicación del sistema jPET para la generación automática de tests en asignaturas de programación con Java
(2016-01) Gómez-Zamalloa Gil, Miguel; Albert Albiol, Elvira; Arenas Sánchez, Purificación; Correas Fernández, Jesús; Genaim, Samir; Román Díez, Guillermo
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-06-30) 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
May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization
(2015-09) Albert Albiol, Elvira; Genaim, Samir; Gordillo, Pablo
A may-happen-in-parallel (MHP) analysis computes pairs of program points that may execute in parallel across different distributed components. This information has been proven to be essential to infer both safety properties (e.g., deadlock freedom) and liveness properties termination and resource boundedness) of asynchronous programs. Existing MHP analyses take advantage of the synchronization points to learn that one task has finished and thus will not happen in parallel with other tasks that are still active. Our starting point is an existing MHP analysis developed for intra-procedural synchronization, i.e., it only allows synchronizing with tasks that have been spawned inside the current task. This paper leverages such MHP analysis to handle inter-procedural synchronization, i.e., a task spawned by one task can be awaited within a different task. This is challenging because task synchronization goes beyond the boundaries of methods, and thus the inference of MHP relations requires novel extensions to capture inter-procedural dependencies. The analysis has been implemented and it can be tried online.
A practical comparator of cost functions and its applications
(Elsevier, 2015-11) Albert Albiol, Elvira; Arenas Sánchez, Purificación; Genaim, Samir; Puebla, Germán
Automatic cost analysis has significantly advanced in the last few years. Nowadays, a number of cost analyzers exist which automatically produce upperand/ or lower-bounds on the amount of resources required to execute a program.Cost analysis has a number of important applications such as resource-usage verification and program synthesis and optimization. For such applications to be successful, it is not suficient to have automatic cost analysis. It is also required to have automated means for handling the analysis results, which are in the form of Cost Functions (CFs for short) i.e., non-recursive expressions composed of a relatively small number of types of basic expressions. In particular, we need automated means for comparing CFs in order to prove that a CF is smaller than or equal to another one for all input values of interest. General function comparison is a hard mathematical problem. Rather than attacking the general problem, in this work we focus on comparing CFs by exploiting their syntactic properties and we present, to the best of our knowledge, the first practical CF comparator which opens the door to fully automated applications of cost analysis. We have implemented the comparator and made its source code available online, so that any cost analyzer can use it.
SACO: Static analyzer for concurrent objects
(Springer, 2014) Albert Albiol, Elvira; Arenas Sánchez, Purificación; Flores Montoya, A.; Genaim, Samir; Gómez-Zamalloa Gil, Miguel; Martín Martín, Enrique; Puebla, G.; Román Díez, Guillermo
We present the main concepts, usage and implementation of SACO, a static analyzer for concurrent objects. Interestingly, SACO is able to infer both liveness(namely termination and resource boundedness) and safety properties (namely deadlock freedom) of programs based on concurrent objects. The system integrates auxiliary analyses such as points-to and may-happen-in-parallel, which are essential for increasing the accuracy of the aforementioned more complex properties. SACO provides accurate information about the dependencies which may introduce deadlocks, loops whose termination is not guaranteed, and upper bounds on the resource consumption of methods.
Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions
(2015-07) Ben-Amran, Amir M., Amir M.; Genaim, Samir
In this paper we turn the spotlight on a class of lexicographic ranking functions introduced by Bradley, Manna and Sipma in a seminal CAV 2005 paper, and establish for the first time the complexity of some problems involving the inference of such functions for linear-constraint loops (without precondition). We show that finding such a function, if one exists, can be done in polynomial time in a way which is sound and complete when the variables range over the rationals (or reals). We show that when variables range over the integers, the problem is harder—deciding the existence of a ranking function is coNP-complete. Next, we study the problem of minimizing the number of components in the ranking function (a.k.a. the dimension). This number is interesting in contexts like computing iteration bounds and loop parallelization. Surprisingly, and unlike the situation for some other classes of lexicographic ranking functions, we find that even deciding whether a two-component ranking function exists is harder than the unrestricted problem: NP-complete over the rationals and Σ P 2 - complete over the integers.
A Transformational Approach to Resource Analysis with Typed-Norms
(2014-12) Albert Albiol, Elvira; Genaim, Samir; Gutiérrez, Raúl
In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along a program's execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent thesizes of the corresponding data. When norms are de_ned by taking typeinformation into account, they are named typed-norms. The main contributionof this paper is a transformational approach to resource analysiswith typed-norms. The analysis is based on a transformation of the programinto an intermediate abstract program in which each variable isabstracted with respect to all considered norms which are valid for itstype. We also sketch a simple analysis that can be used to automaticallyinfer the required, useful, typed-norms from programs.
Conditional Termination of Loops over Heap-Allocated Data
(Elsevier, 2014-10) Albert Albiol, Elvira; 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.
Resource Analysis: From Sequential to Concurrent and Distributed Programs
(2015-06) Albert Albiol, Elvira; Arenas Sánchez, Puri; Correas Fernández, Jesús; Genaim, Samir; Gómez Zamalloa, Miguel; Martín Martín, Enrique; Puebla, Germán; Román Díez, Guillermo
Resource analysis aims at automatically inferring upper/lower bounds on the worst/best-case cost of executing programs. Ideally, a resource analyzer should be parametric on the cost model, i.e., the type of cost that the user wants infer (e.g., number of steps, amount of memory allocated, amount of data transmitted, etc.). The inferred upper bounds have important applications in the fields of program optimization, verification and certification. In this talk, we will review the basic techniques used in resource analysis of sequential programs and the new extensions needed to handle concurrent and distributed systems.