Model Checking and Information Retrieval
URI permanente para esta colección:
Artículos en la categoría Model Checking and Information Retrieval publicados en las Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018).
Notificar un error en esta colección
Examinar
Envíos recientes
Resumen Webpage Menu Detection Based on DOMAlarte Aleixandre, Julián; Insa, David; Sílva, Josep. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.One of the key elements of a website is Web menus, which provide fundamental information about the topology of the own website. Menu detection is useful for humans, but also for crawlers and indexers because the menu provides essential information about the structure and contents of a website. For humans, identifying the main menu of a website is a relatively easy task. However, for computer tools identifying the menu is not trivial at all and, in fact, it is still a challenging unsolved problem. In this work, we propose a novel method for automatic Web menu detection that works at the level of DOM.Resumen Constrained Dynamic Partial Order ReductionActas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.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.Artículo Context-based Model Checking using SMT-solversAbuin, Alex; Díaz de Cerio, Unai; Hermo, Montserrat; Lucio, Paqui. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.In this paper we propose a new idea for the implementation of symbolic model checking. Our pro- posal takes advantage of two technologies. First, SMT-solvers as efficient auxiliary tools to perform a large proportion of the computational task. Second, the context-based tableau that is especially well suited for providing certificates of proved properties, as well as counterexamples of disproved properties. We mainly introduce the algorithm to be implemented, along with illustrative examples.