{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:10:10Z","timestamp":1751663410072,"version":"3.41.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ANR","award":["AAPG TAVA"],"award-info":[{"award-number":["AAPG TAVA"]}]},{"name":"France Strat\u00e9gie 2030","award":["PEPR Cyber Secureval ANR-22-PECY-0005, PEPR Cyber REV ANR-22-PECY-0009"],"award-info":[{"award-number":["PEPR Cyber Secureval ANR-22-PECY-0005, PEPR Cyber REV ANR-22-PECY-0009"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            Most software analysis techniques focus on bug reachability. However, this approach is not ideal for security evaluation as it does not take into account the difficulty of triggering said bugs. The recently introduced notion of\n            <jats:italic toggle=\"yes\">robust reachability<\/jats:italic>\n            tackles this issue by distinguishing between bugs that can be reached independently from uncontrolled inputs, from those that cannot. Yet, this\n            <jats:italic toggle=\"yes\">qualitative<\/jats:italic>\n            notion is too strong in practice as it cannot distinguish mostly replicable bugs from truly unrealistic ones. In this work we propose a more flexible\n            <jats:italic toggle=\"yes\">quantitative<\/jats:italic>\n            version of robust reachability together with a dedicated form of symbolic execution, in order to automatically measure the difficulty of triggering bugs. This\n            <jats:italic toggle=\"yes\">Quantitative Robust Symbolic Execution (QRSE)<\/jats:italic>\n            relies on a variant of model counting, which allows to account for the asymmetry between attacker-controlled and uncontrolled variables. While this specific model counting problem has been studied in AI research fields such as Bayesian networks, knowledge representation and probabilistic planning, its use within the context of formal verification presents new challenges. We show the applicability of our solutions through security-oriented case studies, including real-world vulnerabilities such as CVE-2019-20839 from libvncserver.\n          <\/jats:p>","DOI":"10.1145\/3656407","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"741-765","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Quantitative Robustness for Vulnerability Assessment"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6734-1870","authenticated-orcid":false,"given":"Guillaume","family":"Girol","sequence":"first","affiliation":[{"name":"CEA LIST, Saclay, France"},{"name":"Universit\u00e9 Paris-Saclay, Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-8327-626X","authenticated-orcid":false,"given":"Guilhem","family":"Lacombe","sequence":"additional","affiliation":[{"name":"CEA LIST, Saclay, France"},{"name":"Universit\u00e9 Paris-Saclay, Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6509-3506","authenticated-orcid":false,"given":"S\u00e9bastien","family":"Bardin","sequence":"additional","affiliation":[{"name":"CEA LIST, Saclay, France"},{"name":"Universit\u00e9 Paris-Saclay, Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"[n. d.]. https:\/\/github.com\/LibVNC\/libvncserver. Online accessed November 17th 2023."},{"key":"e_1_3_2_3_1","first-page":"1572","volume-title":"Proceedings of the 43rd International Conference on Software EngineeringIEEE Press","author":"Alshammari Abdulrahman","year":"2021","unstructured":"Abdulrahman Alshammari, Christopher Morris, Michael Hilton, and Jonathan Bell. 2021. FlakeFlagger: Predicting Flakiness Without Rerunning Tests. In Proceedings of the 43rd International Conference on Software Engineering. IEEE Press, 1572\u20131584."},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Abdulbaki Aydin Lucas Bang and Tevfik Bultan. 2015. Automata-Based Model Counting for String Constraints. 255\u2013272. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_15 10.1007\/978-3-319-21690-4_15","DOI":"10.1007\/978-3-319-21690-4_15"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236064"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_75"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_10"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_3"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2012.79"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_14_1","first-page":"1","article-title":"On the Tractable Counting of Theory Models and Its Application to Truth Maintenance and Belief Revision","volume":"11","author":"Darwiche Adnan","year":"2000","unstructured":"Adnan Darwiche. 2000. On the Tractable Counting of Theory Models and Its Application to Truth Maintenance and Belief Revision. Journal of Applied Non-Classical Logics 11 (2000), 1\u20132.","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/502090.502091"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/3000001.3000069"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2016.43"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2003.04.003"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_17"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45477-1_1"},{"key":"e_1_3_2_21_1","first-page":"42","volume-title":"Proceedings, the Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16-20, 2006","author":"Fargier H\u00e9l\u00e8ne","year":"2006","unstructured":"H\u00e9l\u00e8ne Fargier and Pierre Marquis. 2006. On the Use of Partially Ordered Decision Graphs in Knowledge Compilation and Quantified Boolean Formulae. In Proceedings, the Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16-20, 2006, Boston, Massachusetts, USA. AAAI Press, 42\u201347."},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.29007\/dc9b"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v31i1.11138"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336773"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-8147-2_11"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_32"},{"key":"e_1_3_2_27_1","volume-title":"FMSD (CAV special issue)","author":"Girol Guillaume","year":"2022","unstructured":"Guillaume Girol, Benjamin Farinier, and S\u00e9bastien Bardin. 2022. Introducing Robust Reachability. In FMSD (CAV special issue), Alexandra Silva and K. Rustan M. Leino (Eds.). Springer."},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10953315"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_30_1","volume-title":"Handbook of Satisfiability","author":"Gomes Carla P.","year":"2008","unstructured":"Carla P. Gomes, Ashish Sabharwal, and Bart Selman. 2008. Model Counting. In Handbook of Satisfiability. IOS Press."},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04694-0_6"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1920261.1920300"},{"key":"e_1_3_2_34_1","first-page":"253","volume-title":"Proceedings of the Sixteenth International Conference on International Conference on Automated Planning and Scheduling (ICAPS\u201906)","author":"Huang Jinbo","year":"2006","unstructured":"Jinbo Huang. 2006. Combining Knowledge Compilation and Search for Conformant Probabilistic Planning. In Proceedings of the Sixteenth International Conference on International Conference on Automated Planning and Scheduling (ICAPS\u201906). AAAI Press, Cumbria, UK, 253\u2013262."},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89674-6_27"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_8"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254088"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-023-00310-8"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/93"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33011536"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/186"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.505"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635920"},{"key":"e_1_3_2_44_1","first-page":"416","volume-title":"Proceedings of the 20th National Conference on Artificial Intelligence - Volume 1 (AAAI\u201905)","author":"Majercik Stephen M.","year":"2005","unstructured":"Stephen M. Majercik and Byron Boots. 2005. DC-SSAT: A Divide-and-Conquer Approach to Solving Stochastic Satisfiability Problems Efficiently. In Proceedings of the 20th National Conference on Artificial Intelligence - Volume 1 (AAAI\u201905). AAAI Press, Pittsburgh, Pennsylvania, 416\u2013422."},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30353-1_36"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190101"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90045-5"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.8"},{"key":"e_1_3_2_49_1","volume-title":"IJCAI.","author":"Pipatsrisawat Knot","year":"2009","unstructured":"Knot Pipatsrisawat and Adnan Darwiche. 2009. A New D-DNNF-Based Bound Computation Algorithm for Functional E-MAJSAT. In IJCAI."},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2014.34"},{"key":"e_1_3_2_51_1","first-page":"49","volume-title":"Proceedings of the 24th USENIX Conference on Security Symposium (SEC\u201915)","author":"Ramos David A.","year":"2015","unstructured":"David A. Ramos and Dawson Engler. 2015. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In Proceedings of the 24th USENIX Conference on Security Symposium (SEC\u201915). USENIX Association, USA, 49\u201364."},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.26"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","unstructured":"Koushik Sen Darko Marinov and Gul Agha. 2005. CUTE: a concolic unit testing engine for C. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (Lisbon Portugal) (ESEC\/FSE-13). Association for Computing Machinery New York NY USA 263\u2013272. https:\/\/doi.org\/10.1145\/1081706.1081750 10.1145\/1081706.1081750","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_21"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1137\/0208032"},{"key":"e_1_3_2_56_1","first-page":"170","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"Vigouroux Thomas","year":"2022","unstructured":"Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, and Marie-Laure Potet. 2022. BaxMC: a CEGAR approach to Max#SAT. In Formal Methods in Computer-Aided Design (FMCAD). IEEE, 170\u2013178."},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510170"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656407","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656407","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:39:56Z","timestamp":1751661596000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656407"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":56,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656407"],"URL":"https:\/\/doi.org\/10.1145\/3656407","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}