Heuristics for Checking Liveness Properties with Partial Order Reductions
From LRDE
- Authors
- Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Etienne Renault
- Where
- Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16)
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2016-06-17
Abstract
Checking liveness properties with partial-order reductions requires a cycle proviso to ensure that an action cannot be postponed forever. The proviso forces each cycle to contain at least one fully expanded state. We present new heuristics to select which state to expand, hoping to reduce the size of the resulting graph. The choice of the state to expand is done when encountering a dangerous edge. Almost all existing provisos expand the source of this edge, while this paper also explores the expansion of the destination and the use of SCC-based information.
Documents
Bibtex (lrde.bib)
@InProceedings{ duret.16.atva, author = {Alexandre Duret-Lutz and Fabrice Kordon and Denis Poitrenaud and Etienne Renault}, title = {Heuristics for Checking Liveness Properties with Partial Order Reductions}, booktitle = {Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16)}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, volume = {9938}, pages = {340--356}, year = {2016}, month = oct, abstract = {Checking liveness properties with partial-order reductions requires a cycle proviso to ensure that an action cannot be postponed forever. The proviso forces each cycle to contain at least one fully expanded state. We present new heuristics to select which state to expand, hoping to reduce the size of the resulting graph. The choice of the state to expand is done when encountering a \emph{dangerous} edge. Almost all existing provisos expand the source of this edge, while this paper also explores the expansion of the destination and the use of SCC-based information.}, doi = {10.1007/978-3-319-46520-3_22} }