Person:
Isabel Márquez, Miguel

First Name

Miguel

Last Name

Isabel Márquez

URI

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

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 13

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, Georg
The 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.
Generation of Initial Contexts for Effective Deadlock Detection
(2017) Albert Albiol, Elvira María; Isabel Márquez, Miguel; Gómez-Zamalloa Gil, Miguel
It 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.
SYCO: a systematic testing tool for concurrent objects
(2016) Albert Albiol, Elvira María; Isabel Márquez, Miguel; Gómez-Zamalloa Gil, Miguel
We 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.
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, Miguel
Dynamic 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.
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 dynamic partial order reduction and optimality results
(2019) Isabel Márquez, Miguel
Testing concurrent systems requires exploring all possible nondeterministic interleavings that the concurrent execution may have, as any of the interleavings may reveal an erroneous behaviour of the system. This introduces a combinatorial explosion on the number of states that must be considered, which leads often to a computationally intractable problem. In the present PhD thesis, this challenge will be addressed through the development of new Partial Order Reduction techniques (POR). The cornerstone of POR theory is the notion of independence, that is used to decided whether each pair of concurrent events p and t are in a race and thus both executions p · t and t · p must be explored. A fundamental goal of this thesis is to introduce notions of conditional independence –which ensure the commutativity of the considered events p and t under certain conditions that can be evaluated in the explored state– with a DPOR algorithm in order to alleviate the combinatorial explosion problem. The new techniques that we propose in the thesis have been implemented within the SYCO tool. We have carried out accompanying experimental evaluations to prove the effectiveness and applicability of the proposed techniques. Finally, we have successfully verified a range of properties for several case studies of Software-Defined Networks to illustrate the potential of the approach, scaling to larger networks than related techniques.
Deadlock-Guided Testing
(IEEE Access, 2021) Isabel Márquez, Miguel; Gómez-Zamalloa Gil, Miguel; Porfirio Tramontana
Static deadlock analyses might be able to verify the absence of deadlock. However, they are usually not able to detect its presence. Moreover, when a potential deadlock is detected, they provide little (and often no) information that can help the user in finding the source of the anomalous behaviour. This paper proposes a testing methodology that combines static analysis and symbolic execution for effective deadlock detection in asynchronous programs. When the program features a deadlock, our testing methodology provides an effective technique to catch deadlock traces. While if the program does not have deadlock, but the static deadlock analysis inaccurately spotted it, our approach is able to prove deadlock freedom (up to the limit of the performed symbolic exploration).
Deadlock-Guided Testing in CLP
(2017) Isabel Márquez, Miguel; Albert Albiol, Elvira; Gómez-Zamalloa Gil, Miguel
Static deadlock analyzers might be able to verify the absence of deadlock. However, they are usually not able to detect its presence. Also, when they detect a potential deadlock cycle, they provide little (or even no) information on their output. Due to the complex flow of concurrent programs, the user might not be able to find the source of the anomalous behaviour from the abstract information computed by static analysis. This work proposes the combined use of static analysis and testing for effective deadlock detection in asynchronous programs. The asynchronous program is first translated into a CLP-version so that the whole combined approach is carried out by relying on the inherent backtracking mechanism and constraint handling of CLP. When the program features a deadlock, our combined use of analysis and testing provides an effective technique to catch deadlock traces. While if the program does not have deadlock, but the analyzer inaccurately spotted it, we might be able to prove deadlock freedom. The main results in this project have been submitted to: - the special issue on Computational Logic for Verification of the journal Theory and Practice of Logic Programming and - the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'17), and are currently under revision.
Techniques to improve testing scalability on concurrent programs: combining static analysis and testing for Deadlock detection
(2015) Isabel Márquez, Miguel; Albert Albiol, Elvira; Gómez-Zamalloa Gil, Miguel
Static deadlock analyzers might be able to verify the absence of deadlock, but when they detect a potential deadlock cycle, they provide little (or even none) information on their output. Due to the complex ow of concurrent programs, the user might not be able to find the source of the anomalous behaviour from the abstract information computed by static analysis.This paper proposes the combined use of static analysis and testing for effective deadlock detection in asynchronous programs. Our main contributions are: (1)We present an enhanced semantics which allows an early detection of deadlocks during testing and that can give to the user a precise description of the deadlock trace. (2) We combine our testing framework with the abstract descriptions of potential deadlock cycles computed by an existing static deadlock analyzer. Namely, such descriptions are used by our enhanced semantics to guide the execution towards the potential deadlock paths (while other paths are pruned). When the program features a deadlock, our combined use of static analysis and testing provides an effective technique to find deadlock traces. While if the program does not have deadlock, but the analyzer inaccurately spotted it, we might be able to prove deadlock freedom.
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, Alexandra
Software-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.