Context-sensitive dynamic partial order reduction

Elvira Albert, Puri Arenas, María García De La Banda, Miguel Gómez-Zamalloa, Peter J. Stuckey

    Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

    25 Citations (Scopus)


    Dynamic Partial Order Reduction (DPOR) is a powerful technique used in verification and testing to reduce the number of equivalent executions explored. Two executions are equivalent if they can be obtained from each other by swapping adjacent, non-conflicting (inde-pendent) execution steps. Existing DPOR algorithms rely on a notion of independence that is context-insensitive, i.e., the execution steps must be independent in all contexts. In practice, independence is often proved by just checking no execution step writes on a shared variable. We present context-sensitive DPOR, an extension of DPOR that uses context-sensitive independence, where two steps might be independent only in the particular context explored. We show theoretically and experimentally how context-sensitive DPOR can achieve exponential gains.

    Original languageEnglish
    Title of host publicationComputer Aided Verification
    Subtitle of host publication29th International Conference, CAV 2017 Heidelberg, Germany, July 24–28, 2017, Proceedings, Part I
    EditorsRupak Majumdar, Viktor Kunčak
    Place of PublicationBerlin Germany
    Number of pages18
    ISBN (Electronic)9783319633879
    ISBN (Print)9783319633862
    Publication statusPublished - 2017
    EventComputer Aided Verification 2017 - Heidelberg, Germany
    Duration: 24 Jul 201728 Jul 2017
    Conference number: 29th

    Publication series

    NameLecture Notes in Computer Science
    Volume10426 LNCS
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    ConferenceComputer Aided Verification 2017
    Abbreviated titleCAV 2017
    Internet address

    Cite this