Supporting domain-specific state space reductions through local partial-order reduction

Peter Bokor, Johannes Kinder, Marco Serafini, Neeraj Suri

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

Abstract

Model checkers offer to automatically prove safety and liveness properties of complex concurrent software systems, but they are limited by state space explosion. Partial-Order Reduction (POR) is an effective technique to mitigate this burden. However, applying existing notions of POR requires to verify conditions based on execution paths of unbounded length, a difficult task in general. To enable a more intuitive and still flexible application of POR, we propose local POR (LPOR). LPOR is based on the existing notion of statically computed stubborn sets, but its locality allows to verify conditions in single states rather than over long paths. As a case study, we apply LPOR to message-passing systems. We implement it within the Java Pathfinder model checker using our general Java-based LPOR library. Our experiments show significant reductions achieved by LPOR for model checking representative message-passing protocols and, maybe surprisingly, that LPOR can outperform dynamic POR.

Original languageEnglish
Title of host publication2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings
Pages113-122
Number of pages10
DOIs
Publication statusPublished - 1 Dec 2011
Event2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011 - Lawrence, KS, United States
Duration: 6 Nov 201110 Nov 2011

Publication series

Name2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings

Other

Other2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011
CountryUnited States
CityLawrence, KS
Period6/11/1110/11/11

    Fingerprint

ASJC Scopus subject areas

  • Software

Cite this

Bokor, P., Kinder, J., Serafini, M., & Suri, N. (2011). Supporting domain-specific state space reductions through local partial-order reduction. In 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings (pp. 113-122). [6100044] (2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings). https://doi.org/10.1109/ASE.2011.6100044