Optimal context-sensitive Dynamic Partial Order Reduction with observers

Elvira Albert, Maria Garcia De La Banda, Miguel Gómez-Zamalloa, Miguel Isabel, Peter J. Stuckey

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

1 Citation (Scopus)

Abstract

Dynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking to avoid the exploration of equivalent execution sequences. DPOR relies on the notion of independence between execution steps to detect equivalence. Recent progress in the area has introduced more accurate ways to detect independence: Context-Sensitive DPOR considers two steps p and t independent in the current state if the states obtained by executing p · t and t · p are the same; Optimal DPOR with Observers makes their dependency conditional to the existence of future events that observe their operations. We introduce a new algorithm, Optimal Context-Sensitive DPOR with Observers, that combines these two notions of conditional independence, and goes beyond them by exploiting their synergies. Experimental evaluation shows that our gains increase exponentially with the size of the considered inputs.

Original languageEnglish
Title of host publicationProceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis
EditorsDongmei Zhang, Anders Moller
Place of PublicationNew York NY USA
PublisherAssociation for Computing Machinery (ACM)
Pages352-362
Number of pages11
ISBN (Electronic)9781450362245
DOIs
Publication statusPublished - 2019
EventInternational Symposium on Software Testing and Analysis 2019 - Beijing, China
Duration: 15 Jul 201919 Jul 2019
Conference number: 28th
https://conf.researchr.org/home/issta-2019

Conference

ConferenceInternational Symposium on Software Testing and Analysis 2019
Abbreviated titleISSTA 2019
CountryChina
CityBeijing
Period15/07/1919/07/19
Internet address

Keywords

  • Model-Checking
  • Partial-Order Reduction
  • Software Verification
  • Testing

Cite this

Albert, E., De La Banda, M. G., Gómez-Zamalloa, M., Isabel, M., & Stuckey, P. J. (2019). Optimal context-sensitive Dynamic Partial Order Reduction with observers. In D. Zhang, & A. Moller (Eds.), Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis (pp. 352-362). New York NY USA: Association for Computing Machinery (ACM). https://doi.org/10.1145/3293882.3330565
Albert, Elvira ; De La Banda, Maria Garcia ; Gómez-Zamalloa, Miguel ; Isabel, Miguel ; Stuckey, Peter J. / Optimal context-sensitive Dynamic Partial Order Reduction with observers. Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. editor / Dongmei Zhang ; Anders Moller. New York NY USA : Association for Computing Machinery (ACM), 2019. pp. 352-362
@inproceedings{5bd4bc6461814ccd9b5f627f3110df29,
title = "Optimal context-sensitive Dynamic Partial Order Reduction with observers",
abstract = "Dynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking to avoid the exploration of equivalent execution sequences. DPOR relies on the notion of independence between execution steps to detect equivalence. Recent progress in the area has introduced more accurate ways to detect independence: Context-Sensitive DPOR considers two steps p and t independent in the current state if the states obtained by executing p · t and t · p are the same; Optimal DPOR with Observers makes their dependency conditional to the existence of future events that observe their operations. We introduce a new algorithm, Optimal Context-Sensitive DPOR with Observers, that combines these two notions of conditional independence, and goes beyond them by exploiting their synergies. Experimental evaluation shows that our gains increase exponentially with the size of the considered inputs.",
keywords = "Model-Checking, Partial-Order Reduction, Software Verification, Testing",
author = "Elvira Albert and {De La Banda}, {Maria Garcia} and Miguel G{\'o}mez-Zamalloa and Miguel Isabel and Stuckey, {Peter J.}",
year = "2019",
doi = "10.1145/3293882.3330565",
language = "English",
pages = "352--362",
editor = "Dongmei Zhang and Anders Moller",
booktitle = "Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis",
publisher = "Association for Computing Machinery (ACM)",
address = "United States of America",

}

Albert, E, De La Banda, MG, Gómez-Zamalloa, M, Isabel, M & Stuckey, PJ 2019, Optimal context-sensitive Dynamic Partial Order Reduction with observers. in D Zhang & A Moller (eds), Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. Association for Computing Machinery (ACM), New York NY USA, pp. 352-362, International Symposium on Software Testing and Analysis 2019, Beijing, China, 15/07/19. https://doi.org/10.1145/3293882.3330565

Optimal context-sensitive Dynamic Partial Order Reduction with observers. / Albert, Elvira; De La Banda, Maria Garcia; Gómez-Zamalloa, Miguel; Isabel, Miguel; Stuckey, Peter J.

Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. ed. / Dongmei Zhang; Anders Moller. New York NY USA : Association for Computing Machinery (ACM), 2019. p. 352-362.

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

TY - GEN

T1 - Optimal context-sensitive Dynamic Partial Order Reduction with observers

AU - Albert, Elvira

AU - De La Banda, Maria Garcia

AU - Gómez-Zamalloa, Miguel

AU - Isabel, Miguel

AU - Stuckey, Peter J.

PY - 2019

Y1 - 2019

N2 - Dynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking to avoid the exploration of equivalent execution sequences. DPOR relies on the notion of independence between execution steps to detect equivalence. Recent progress in the area has introduced more accurate ways to detect independence: Context-Sensitive DPOR considers two steps p and t independent in the current state if the states obtained by executing p · t and t · p are the same; Optimal DPOR with Observers makes their dependency conditional to the existence of future events that observe their operations. We introduce a new algorithm, Optimal Context-Sensitive DPOR with Observers, that combines these two notions of conditional independence, and goes beyond them by exploiting their synergies. Experimental evaluation shows that our gains increase exponentially with the size of the considered inputs.

AB - Dynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking to avoid the exploration of equivalent execution sequences. DPOR relies on the notion of independence between execution steps to detect equivalence. Recent progress in the area has introduced more accurate ways to detect independence: Context-Sensitive DPOR considers two steps p and t independent in the current state if the states obtained by executing p · t and t · p are the same; Optimal DPOR with Observers makes their dependency conditional to the existence of future events that observe their operations. We introduce a new algorithm, Optimal Context-Sensitive DPOR with Observers, that combines these two notions of conditional independence, and goes beyond them by exploiting their synergies. Experimental evaluation shows that our gains increase exponentially with the size of the considered inputs.

KW - Model-Checking

KW - Partial-Order Reduction

KW - Software Verification

KW - Testing

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

U2 - 10.1145/3293882.3330565

DO - 10.1145/3293882.3330565

M3 - Conference Paper

SP - 352

EP - 362

BT - Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis

A2 - Zhang, Dongmei

A2 - Moller, Anders

PB - Association for Computing Machinery (ACM)

CY - New York NY USA

ER -

Albert E, De La Banda MG, Gómez-Zamalloa M, Isabel M, Stuckey PJ. Optimal context-sensitive Dynamic Partial Order Reduction with observers. In Zhang D, Moller A, editors, Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. New York NY USA: Association for Computing Machinery (ACM). 2019. p. 352-362 https://doi.org/10.1145/3293882.3330565