Person: Albert Albiol, Elvira María
Loading...
First Name
Elvira María
Last Name
Albert Albiol
Affiliation
Universidad Complutense de Madrid
Faculty / Institute
Informática
Department
Sistemas Informáticos y Computación
Area
Lenguajes y Sistemas Informáticos
Identifiers
13 results
Search Results
Now showing 1 - 10 of 13
Item SACO: Static analyzer for concurrent objects(Lecture Notes in Computer Science, 2014) Albert Albiol, Elvira María; 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, GuillermoWe 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.Item Systematic testing of actor systems(Journal of Software Testing Verification and Reliability, 2018) Albert Albiol, Elvira María; Arenas Sánchez, Purificación; Gómez-Zamalloa Gil, MiguelTesting concurrent systems requires exploring all possible nondeterministic interleavings that the concurrent execution may have, as any of the interleavings may reveal the erroneous behavior. In testing of actor systems, we can distinguish 2 sources of nondeterminism: (1) actor selection, the order in which actors are explored, and (2) task selection, the order in which the tasks within each actor are explored. This article provides new strategies and heuristics for pruning redundant state-exploration when testing actor systems by reducing the amount of unnecessary nondeterminism of both types. Furthermore, we extend these techniques to handle synchronization primitives that allow awaiting for the completion of an asynchronous task.We report on an implementation and experimental evaluation of the proposed techniques in SYCO, a testing tool for actor-based concurrency.Item Constrained Dynamic Partial Order Reduction(2018) Albert Albiol, Elvira María; Gómez-Zamalloa Gil, Miguel; Isabel Márquez, Miguel; Rubio, Albert; Chockler, Hana; Weissenbacher, GeorgThe cornerstone of dynamic partial order reduction (DPOR) is the notion of independence that is used to decide whether each pair of concurrent events p and t are in a race and thus both p · t and t · p must be explored. We present constrained dynamic partial order reduction (CDPOR), an extension of the DPOR framework which is able to avoid redundant explorations based on the notion of conditional independence— the execution of p and t commutes only when certain independence constraints (ICs) are satisfied. ICs can be declared by the programmer, but importantly, we present a novel SMT-based approach to automatically synthesize ICs in a static pre-analysis. A unique feature of our approach is that we have succeeded to exploit ICs within the state-of-the-art DPOR algorithm, achieving exponential reductions over existing implementations.Item Generation of Initial Contexts for Effective Deadlock Detection(2017) Albert Albiol, Elvira María; Isabel Márquez, Miguel; Gómez-Zamalloa Gil, MiguelIt has been recently proposed that testing based on symbolic execution can be used in conjunction with static deadlock analysis to define a deadlock detection framework that: (i) can show deadlock presence, in that case a concrete test-case and trace are obtained, and (ii) can also prove deadlock freedom. Such symbolic execution starts from an initial distributed context, i.e., a set of locations and their initial tasks. Considering all possibilities results in a combinatorial explosion on the different distributed contexts that must be considered. This paper proposes a technique to effectively generate initial contexts that can lead to deadlock, using the possible conflicting task interactions identified by static analysis, discarding other distributed contexts that cannot lead to deadlock. The proposed technique has been integrated in the above-mentioned deadlock detection framework hence enabling it to analyze systems without the need of any user supplied initial context.Item SYCO: a systematic testing tool for concurrent objects(2016) Albert Albiol, Elvira María; Isabel Márquez, Miguel; Gómez-Zamalloa Gil, MiguelWe present the concepts, usage and prototypical implementation of SYCO: a SYstematic testing tool for Concurrent Objects. The system receives as input a program, a selection of method to be tested, and a set of initial values for its parameters. SYCO offers a visual web interface to carry out the testing process and visualize the results of the different executions as well as the sequences of tasks scheduled as a sequence diagram. Its kernel includes state-of-theart partial-order reduction techniques to avoid redundant computations during testing. Besides, SYCO incorporates an option to effectively catch deadlock errors. In particular, it uses advanced techniques which guide the execution towards potential deadlock paths and discard paths that are guaranteed to be deadlock free.- Project number: 245
Item 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, ClaraEl 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
Item 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 Item Optimal dynamic partial order reduction with context-sensitive independence and observers(Journal of Systems and Software, 2023) Albert Albiol, Elvira María; Garcia de la Banda, María; Isabel Márquez, Miguel; Stuckey, Peter J.; Gómez-Zamalloa Gil, MiguelDynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking of concurrent programs to avoid the exploration of equivalent execution sequences. In order to detect equivalence, DPOR relies on the notion of independence between execution steps. As this notion must be approximated, it can lose precision and thus treat execution steps as interfering when they are not. Our work is inspired by recent progress in the area that has introduced more accurate ways to exploit conditional notions of independence: Context-Sensitive DPOR considers two steps p and t independent in the current state if the states obtained by executing p · t and t · p are the same; Optimal DPOR with Observers makes their dependency conditional to the existence of future events that observe their operations. This article introduces a new algorithm, Optimal Context-Sensitive DPOR with Observers, that combines these two notions of conditional independence, and goes beyond them by exploiting their synergies. The implementation of our algorithm has been undertaken within the Nidhugg model checking tool. Our experimental evaluation, using benchmarks from the previous works, shows that our algorithm is able to effectively combine the benefits of both context-sensitive and observers-based independence and that it can produce exponential reductions over both of them.Item SDN-Actors: Modeling and Verification of SDN Programs(2018) Albert Albiol, Elvira María; Rubio, Albert; Sammartino, Matteo; Silva, Alexandra; Gómez-Zamalloa Gil, MiguelSoftware-Defined Networking (SDN) is a recent networking paradigm that has become increasingly popular in the last decade. It gives unprecedented control over the global behavior of the network and provides a new opportunity for formal methods. Much work has appeared in the last few years on providing bridges between SDN and verification. This paper advances this research line and provides a link between SDN and traditional work on formal methods for verification of distributed software—actor-based modelling. We show how SDN programs can be seamlessly modelled using actors, and thus existing advanced model checking techniques developed for actors can be directly applied to verify a range of properties of SDN networks, including consistency of flow tables, violation of safety policies, and forwarding loops.Item Actor-based model checking for Software-Defined Networks(Journal of Logical and Algebraic Methods in Programming, 2021) Albert Albiol, Elvira María; Gómez-Zamalloa Gil, Miguel; Isabel Márquez, Miguel; Rubio, Albert; Sammartino, Matteo; Silva, AlexandraSoftware-Defined Networking (SDN) is a networking paradigm that has become increasingly popular in the last decade. The unprecedented control over the global behaviour of the network it provides opens a range of new opportunities for formal methods and much work has appeared in the last few years on providing bridges between SDN and verification. This article advances this research line and provides a link between SDN and traditional work on formal methods for verification of concurrent and distributed software—actor-based modelling. We show how SDN programs can be seamlessly modelled using actors, and thus existing advanced model checking techniques developed for actors can be directly applied to verify a range of properties of SDNs, including consistency of flow tables, violation of safety policies, and forwarding loops. Our model checker for SDNs is available through an online web interface, that also provides the SDN actor-models for a number of well-known SDN benchmarks.