Standard

Uniform Sampling of SAT Solutions for Configurable Systems : Are We There Yet? / Plazar, Quentin; Acher, Mathieu; Perrouin, Gilles; Devroey, Xavier; Cordy, Maxime.

2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST): Proceedings. ed. / L. O'Conner. Piscataway, NJ : IEEE, 2019. p. 240-251.

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

Harvard

Plazar, Q, Acher, M, Perrouin, G, Devroey, X & Cordy, M 2019, Uniform Sampling of SAT Solutions for Configurable Systems: Are We There Yet? in L O'Conner (ed.), 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST): Proceedings. IEEE, Piscataway, NJ, pp. 240-251, ICST 2019 , Xi'an, China, 22/04/19. https://doi.org/10.1109/ICST.2019.00032

APA

Plazar, Q., Acher, M., Perrouin, G., Devroey, X., & Cordy, M. (2019). Uniform Sampling of SAT Solutions for Configurable Systems: Are We There Yet? In L. O'Conner (Ed.), 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST): Proceedings (pp. 240-251). Piscataway, NJ: IEEE. https://doi.org/10.1109/ICST.2019.00032

Vancouver

Plazar Q, Acher M, Perrouin G, Devroey X, Cordy M. Uniform Sampling of SAT Solutions for Configurable Systems: Are We There Yet? In O'Conner L, editor, 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST): Proceedings. Piscataway, NJ: IEEE. 2019. p. 240-251 https://doi.org/10.1109/ICST.2019.00032

Author

Plazar, Quentin ; Acher, Mathieu ; Perrouin, Gilles ; Devroey, Xavier ; Cordy, Maxime. / Uniform Sampling of SAT Solutions for Configurable Systems : Are We There Yet?. 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST): Proceedings. editor / L. O'Conner. Piscataway, NJ : IEEE, 2019. pp. 240-251

BibTeX

@inproceedings{f568f3328fa84b798b90304b063bfb94,
title = "Uniform Sampling of SAT Solutions for Configurable Systems: Are We There Yet?",
abstract = "Uniform or near-uniform generation of solutions for large satisfiability formulas is a problem of theoretical and practical interest for the testing community. Recent works proposed two algorithms (namely UniGen and QuickSampler) for reaching a good compromise between execution time and uniformity guarantees, with empirical evidence on SAT benchmarks. In the context of highly-configurable software systems (e.g., Linux), it is unclear whether UniGen and QuickSampler can scale and sample uniform software configurations. In this paper, we perform a thorough experiment on 128 real-world feature models. We find that UniGen is unable to produce SAT solutions out of such feature models. Furthermore, we show that QuickSampler does not generate uniform samples and that some features are either never part of the sample or too frequently present. Finally, using a case study, we characterize the impacts of these results on the ability to find bugs in a configurable system. Overall, our results suggest that we are not there: more research is needed to explore the cost-effectiveness of uniform sampling when testing large configurable systems.",
author = "Quentin Plazar and Mathieu Acher and Gilles Perrouin and Xavier Devroey and Maxime Cordy",
note = "Accepted author manuscript",
year = "2019",
doi = "10.1109/ICST.2019.00032",
language = "English",
isbn = "978-1-7281-1737-9",
pages = "240--251",
editor = "L. O'Conner",
booktitle = "2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST)",
publisher = "IEEE",

}

RIS

TY - GEN

T1 - Uniform Sampling of SAT Solutions for Configurable Systems

T2 - Are We There Yet?

AU - Plazar, Quentin

AU - Acher, Mathieu

AU - Perrouin, Gilles

AU - Devroey, Xavier

AU - Cordy, Maxime

N1 - Accepted author manuscript

PY - 2019

Y1 - 2019

N2 - Uniform or near-uniform generation of solutions for large satisfiability formulas is a problem of theoretical and practical interest for the testing community. Recent works proposed two algorithms (namely UniGen and QuickSampler) for reaching a good compromise between execution time and uniformity guarantees, with empirical evidence on SAT benchmarks. In the context of highly-configurable software systems (e.g., Linux), it is unclear whether UniGen and QuickSampler can scale and sample uniform software configurations. In this paper, we perform a thorough experiment on 128 real-world feature models. We find that UniGen is unable to produce SAT solutions out of such feature models. Furthermore, we show that QuickSampler does not generate uniform samples and that some features are either never part of the sample or too frequently present. Finally, using a case study, we characterize the impacts of these results on the ability to find bugs in a configurable system. Overall, our results suggest that we are not there: more research is needed to explore the cost-effectiveness of uniform sampling when testing large configurable systems.

AB - Uniform or near-uniform generation of solutions for large satisfiability formulas is a problem of theoretical and practical interest for the testing community. Recent works proposed two algorithms (namely UniGen and QuickSampler) for reaching a good compromise between execution time and uniformity guarantees, with empirical evidence on SAT benchmarks. In the context of highly-configurable software systems (e.g., Linux), it is unclear whether UniGen and QuickSampler can scale and sample uniform software configurations. In this paper, we perform a thorough experiment on 128 real-world feature models. We find that UniGen is unable to produce SAT solutions out of such feature models. Furthermore, we show that QuickSampler does not generate uniform samples and that some features are either never part of the sample or too frequently present. Finally, using a case study, we characterize the impacts of these results on the ability to find bugs in a configurable system. Overall, our results suggest that we are not there: more research is needed to explore the cost-effectiveness of uniform sampling when testing large configurable systems.

U2 - 10.1109/ICST.2019.00032

DO - 10.1109/ICST.2019.00032

M3 - Conference contribution

SN - 978-1-7281-1737-9

SP - 240

EP - 251

BT - 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST)

A2 - O'Conner, L.

PB - IEEE

CY - Piscataway, NJ

ER -

ID: 50255280