Home > Research > Publications & Outputs > Supporting domain-specific state space reductio...

Research

Associated organisational units

Links

Text available via DOI:

Keywords

View graph of relations

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

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Published

Standard

Supporting domain-specific state space reductions through local partial-order reduction. / Bokor, P.; Kinder, J.; Serafini, M. et al.
2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011). IEEE, 2011. p. 113-122.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

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). IEEE, pp. 113-122. https://doi.org/10.1109/ASE.2011.6100044

APA

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) (pp. 113-122). IEEE. https://doi.org/10.1109/ASE.2011.6100044

Vancouver

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

Author

Bokor, P. ; Kinder, J. ; Serafini, M. et al. / Supporting domain-specific state space reductions through local partial-order reduction. 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011). IEEE, 2011. pp. 113-122

Bibtex

@inproceedings{0277de81151548149005a2abc908d293,
title = "Supporting domain-specific state space reductions through local partial-order reduction",
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. {\textcopyright} 2011 IEEE.",
keywords = "Concurrent software systems, Domain specific, Execution paths, Java PathFinder, Liveness properties, Long-path, Message passing systems, Model checker, Partial-order reduction, Single state, State-space explosion, State-space reduction, Stubborn sets, Message passing, Software engineering, Model checking",
author = "P. Bokor and J. Kinder and M. Serafini and Neeraj Suri",
year = "2011",
month = nov,
day = "6",
doi = "10.1109/ASE.2011.6100044",
language = "English",
isbn = "9781457716386",
pages = "113--122",
booktitle = "2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)",
publisher = "IEEE",

}

RIS

TY - GEN

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

AU - Bokor, P.

AU - Kinder, J.

AU - Serafini, M.

AU - Suri, Neeraj

PY - 2011/11/6

Y1 - 2011/11/6

N2 - 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. © 2011 IEEE.

AB - 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. © 2011 IEEE.

KW - Concurrent software systems

KW - Domain specific

KW - Execution paths

KW - Java PathFinder

KW - Liveness properties

KW - Long-path

KW - Message passing systems

KW - Model checker

KW - Partial-order reduction

KW - Single state

KW - State-space explosion

KW - State-space reduction

KW - Stubborn sets

KW - Message passing

KW - Software engineering

KW - Model checking

U2 - 10.1109/ASE.2011.6100044

DO - 10.1109/ASE.2011.6100044

M3 - Conference contribution/Paper

SN - 9781457716386

SP - 113

EP - 122

BT - 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)

PB - IEEE

ER -