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

    Abstract

    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.

    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
    PublisherSpringer-Verlag London Ltd.
    Pages526-543
    Number of pages18
    ISBN (Electronic)9783319633879
    ISBN (Print)9783319633862
    DOIs
    StatePublished - 2017
    Event29th International Conference on Computer Aided Verification, CAV 2017 - Heidelberg, Germany
    Duration: 24 Jul 201728 Jul 2017

    Publication series

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

    Conference

    Conference29th International Conference on Computer Aided Verification, CAV 2017
    CountryGermany
    CityHeidelberg
    Period24/07/1728/07/17

    Cite this

    Albert, E., Arenas, P., De La Banda, M. G., Gómez-Zamalloa, M., & Stuckey, P. J. (2017). Context-sensitive dynamic partial order reduction. In R. Majumdar, & V. Kunčak (Eds.), Computer Aided Verification : 29th International Conference, CAV 2017 Heidelberg, Germany, July 24–28, 2017, Proceedings, Part I (pp. 526-543). (Lecture Notes in Computer Science ; Vol. 10426 LNCS). Springer-Verlag London Ltd.. DOI: 10.1007/978-3-319-63387-9_26
    Albert, Elvira ; Arenas, Puri ; De La Banda, María García ; Gómez-Zamalloa, Miguel ; Stuckey, Peter J./ Context-sensitive dynamic partial order reduction. Computer Aided Verification : 29th International Conference, CAV 2017 Heidelberg, Germany, July 24–28, 2017, Proceedings, Part I. editor / Rupak Majumdar ; Viktor Kunčak. Springer-Verlag London Ltd., 2017. pp. 526-543 (Lecture Notes in Computer Science ).
    @inproceedings{d6411fd12c80435b8c3742b6f0f1edc7,
    title = "Context-sensitive dynamic partial order reduction",
    abstract = "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.",
    author = "Elvira Albert and Puri Arenas and {De La Banda}, {Mar{\'i}a Garc{\'i}a} and Miguel G{\'o}mez-Zamalloa and Stuckey, {Peter J.}",
    year = "2017",
    doi = "10.1007/978-3-319-63387-9_26",
    language = "English",
    isbn = "9783319633862",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer-Verlag London Ltd.",
    pages = "526--543",
    editor = "Majumdar, {Rupak } and Kunčak, {Viktor }",
    booktitle = "Computer Aided Verification",
    address = "Germany",

    }

    Albert, E, Arenas, P, De La Banda, MG, Gómez-Zamalloa, M & Stuckey, PJ 2017, Context-sensitive dynamic partial order reduction. in R Majumdar & V Kunčak (eds), Computer Aided Verification : 29th International Conference, CAV 2017 Heidelberg, Germany, July 24–28, 2017, Proceedings, Part I. Lecture Notes in Computer Science , vol. 10426 LNCS, Springer-Verlag London Ltd., pp. 526-543, 29th International Conference on Computer Aided Verification, CAV 2017, Heidelberg, Germany, 24/07/17. DOI: 10.1007/978-3-319-63387-9_26

    Context-sensitive dynamic partial order reduction. / Albert, Elvira; Arenas, Puri; De La Banda, María García; Gómez-Zamalloa, Miguel; Stuckey, Peter J.

    Computer Aided Verification : 29th International Conference, CAV 2017 Heidelberg, Germany, July 24–28, 2017, Proceedings, Part I. ed. / Rupak Majumdar; Viktor Kunčak. Springer-Verlag London Ltd., 2017. p. 526-543 (Lecture Notes in Computer Science ; Vol. 10426 LNCS).

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

    TY - GEN

    T1 - Context-sensitive dynamic partial order reduction

    AU - Albert,Elvira

    AU - Arenas,Puri

    AU - De La Banda,María García

    AU - Gómez-Zamalloa,Miguel

    AU - Stuckey,Peter J.

    PY - 2017

    Y1 - 2017

    N2 - 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.

    AB - 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.

    UR - http://www.scopus.com/inward/record.url?scp=85026725294&partnerID=8YFLogxK

    U2 - 10.1007/978-3-319-63387-9_26

    DO - 10.1007/978-3-319-63387-9_26

    M3 - Conference Paper

    SN - 9783319633862

    T3 - Lecture Notes in Computer Science

    SP - 526

    EP - 543

    BT - Computer Aided Verification

    PB - Springer-Verlag London Ltd.

    ER -

    Albert E, Arenas P, De La Banda MG, Gómez-Zamalloa M, Stuckey PJ. Context-sensitive dynamic partial order reduction. In Majumdar R, Kunčak V, editors, Computer Aided Verification : 29th International Conference, CAV 2017 Heidelberg, Germany, July 24–28, 2017, Proceedings, Part I. Springer-Verlag London Ltd.2017. p. 526-543. (Lecture Notes in Computer Science ). Available from, DOI: 10.1007/978-3-319-63387-9_26