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

5 Citations (Scopus)


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)
Number of pages11
ISBN (Electronic)9781450362245
Publication statusPublished - 2019
EventInternational Symposium on Software Testing and Analysis 2019 - Beijing, China
Duration: 15 Jul 201919 Jul 2019
Conference number: 28th


ConferenceInternational Symposium on Software Testing and Analysis 2019
Abbreviated titleISSTA 2019
Internet address


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

Cite this