Person:
Isabel Márquez, Miguel

Profile Picture
First Name
Miguel
Last Name
Isabel Márquez
Affiliation
Universidad Complutense de Madrid
Faculty / Institute
Informática
Department
Sistemas Informáticos y Computación
Area
Lenguajes y Sistemas Informáticos
Identifiers
UCM identifierScopus Author IDDialnet ID

Filters

2015 - 201922020 - 20211
Reset filters

Settings

Search Results

Now showing 1 - 3 of 3
  • Thumbnail Image
    Publication
    Verificacion de Sistemas Concurrentes: optimalidad, Escalabilidad y Aplicabilidad
    (Universidad Complutense de Madrid, 2021-05-28) Isabel Márquez, Miguel; Albert Albiol, Elvira; Gómez-Zamalloa Gil, Miguel
    Tanto el testing como la verificacion de sistemas concurrentes requieren explorar todos los posibles entrelazados no deterministas que la ejecucion concurrente puede tener, ya que cualquiera de estos entrelazados podra revelar un comportamiento erroneo del sistema. Esto introduce una explosion combinatoria en el numero de estados del programa que deben ser considerados, lo que frecuentemente lleva a un problema computacionalmente intratable. El objetivo de esta tesis es el desarrollo de tecnicas novedosas para el testing y la verificacion de programas concurrentes que permitan reducir esta explosion combinatoria...
  • Thumbnail Image
    Publication
    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.
  • Thumbnail Image
    Publication
    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.