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 Paper

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 Paper

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