{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T04:12:37Z","timestamp":1751688757510,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ANR","award":["ANR-10-AIRT-05, ANR-22-PECY-0005, ANR-22-PECY-0009"],"award-info":[{"award-number":["ANR-10-AIRT-05, ANR-22-PECY-0005, 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,1,2]]},"abstract":"<jats:p>\n            Characterization of bugs and attack vectors is in many practical scenarios as important as their finding. Recently, Girol\n            <jats:italic toggle=\"yes\">et al.<\/jats:italic>\n            have introduced the concept of\n            <jats:italic toggle=\"yes\">robust reachability<\/jats:italic>\n            , which ensures a perfect\n            <jats:italic toggle=\"yes\">reproducibility<\/jats:italic>\n            of the reported violations by distinguishing inputs that are under the control of the attacker (\n            <jats:italic toggle=\"yes\">controlled inputs<\/jats:italic>\n            ) from those that are not (\n            <jats:italic toggle=\"yes\">uncontrolled inputs<\/jats:italic>\n            ), and proposed first automated analysis for it. While it is a step toward distinguishing severe bugs from benign ones, it fails for example to describe violations that are\n            <jats:italic toggle=\"yes\">mostly<\/jats:italic>\n            reproducible, i.e., when triggering conditions are likely to happen, meaning that they happen for all uncontrolled inputs but a few corner cases. To address this issue, we propose to leverage theory-agnostic abduction techniques to generate\n            <jats:italic toggle=\"yes\">constraints on the uncontrolled program inputs that ensure that a target property is robustly satisfied<\/jats:italic>\n            . Our proposal comes with an extension of robust reachability that is generic on the type of trace property and on the technology used to verify the properties. We show that our approach is complete\n            <jats:italic toggle=\"yes\">w.r.t.<\/jats:italic>\n            its\n            <jats:italic toggle=\"yes\">inference language<\/jats:italic>\n            , and we additionally discuss strategies for the efficient exploration of the inference space. We demonstrate the feasibility of the method and its practical ability to refine the notion of robust reachability with an implementation that uses robust reachability oracles to generate constraints on standard benchmarks from software verification and security analysis. We illustrate the use of our implementation to a vulnerability characterization problem in the context of fault injection attacks. Our method overcomes a major limitation of the initial proposal of robust reachability, without complicating its definition. From a practical view, this is a step toward new verification tools that are able to characterize program violations through high-level feedback.\n          <\/jats:p>","DOI":"10.1145\/3632933","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2731-2760","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Inference of Robust Reachability Constraints"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-8833-3863","authenticated-orcid":false,"given":"Yanis","family":"Sellami","sequence":"first","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, CEA, List, Grenoble, France"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6734-1870","authenticated-orcid":false,"given":"Guillaume","family":"Girol","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Saclay, CEA, List, Palaiseau, France"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-9736-0656","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Recoules","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Saclay, CEA, List, Palaiseau, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2761-3627","authenticated-orcid":false,"given":"Damien","family":"Courouss\u00e9","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, CEA, List, Grenoble, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6509-3506","authenticated-orcid":false,"given":"S\u00e9bastien","family":"Bardin","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Saclay, CEA, List, Palaiseau, France"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"Aws Albarghouthi Isil Dillig and Arie Gurfinkel. 2016. Maximal Specification Synthesis. In POPL. https:\/\/doi.org\/10.1145\/2837614.2837628 10.1145\/2837614.2837628","DOI":"10.1145\/2837614.2837628"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","unstructured":"Angello Astorga Siwakorn Srisakaokul Xusheng Xiao and Tao Xie. 2018. PreInfer: Automatic Inference of Preconditions via Symbolic Analysis. DSN (2018). https:\/\/doi.org\/10.1109\/DSN.2018.00074 10.1109\/DSN.2018.00074","DOI":"10.1109\/DSN.2018.00074"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Rehan Abdul Aziz Geoffrey Chu Christian Muise and Peter Stuckey. 2015. #\u2203SAT: Projected Model Counting. In Theory and Applications of Satisfiability Testing \u2013 SAT. https:\/\/doi.org\/10.1007\/978-3-319-24318-4_10 10.1007\/978-3-319-24318-4_10","DOI":"10.1007\/978-3-319-24318-4_10"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"Haniel Barbosa Clark W. Barrett Martin Brain Gereon Kremer Hanna Lachnitt Makai Mann Abdalrhman Mohamed Mudathir Mohamed Aina Niemetz Andres N\u00f6tzli Alex Ozdemir Mathias Preiner Andrew Reynolds Ying Sheng Cesare Tinelli and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In TACAS. https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24 10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"S\u00e9bastien Bardin and Guillaume Girol. 2022. A Quantitative Flavour of Robust Reachability. https:\/\/doi.org\/10.48550\/ARXIV.2212.05244 10.48550\/ARXIV.2212.05244","DOI":"10.48550\/ARXIV.2212.05244"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Clark Barrett Roberto Sebastiani Sanjit A. Seshia and Cesare Tinelli. 2009. Satisfiability modulo theories. https:\/\/doi.org\/10.3233\/978-1-58603-929-5-825 10.3233\/978-1-58603-929-5-825","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Dirk Beyer. 2012. Competition on Software Verification (SV-COMP). In TACAS. https:\/\/doi.org\/10.1007\/978-3-642-28756-5_38 10.1007\/978-3-642-28756-5_38","DOI":"10.1007\/978-3-642-28756-5_38"},{"key":"e_1_3_1_9_1","unstructured":"Meghyn Bienvenu. 2007. Prime Implicates and Prime Implicants in Modal Logic. In AAAI."},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Cristian Cadar and Koushik Sen. 2013. Symbolic Execution for Software Testing: Three Decades Later. Commun. ACM (2013). https:\/\/doi.org\/10.1145\/2408776.2408795 10.1145\/2408776.2408795","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1002\/9781118604182"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Cristiano Calcagno Dino Distefano Peter O\u2019Hearn and Hongseok Yang. 2009. Compositional Shape Analysis by Means of Bi-Abduction. J. ACM (2009). https:\/\/doi.org\/10.1145\/2049697.2049700 10.1145\/2049697.2049700","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Edmund M. Clarke Daniel Kroening and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In TACAS. https: \/\/doi.org\/10.1007\/978-3-540-24730-2_15 10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Patrick Cousot Radhia Cousot Manuel F\u00e4hndrich and Francesco Logozzo. 2013. Automatic Inference of Necessary Preconditions. In VMCAI. https:\/\/doi.org\/10.1007\/978-3-642-35873-9_10 10.1007\/978-3-642-35873-9_10","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Lesly-Ann Daniel S\u00e9bastien Bardin and Tamara Rezk. 2020. Binsec\/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level. In IEEE SP. https:\/\/doi.org\/10.1109\/SP40000.2020.00074 10.1109\/SP40000.2020.00074","DOI":"10.1109\/SP40000.2020.00074"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","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 (2000). https:\/\/doi.org\/10.3166\/jancl.11.11-34 10.3166\/jancl.11.11-34","DOI":"10.3166\/jancl.11.11-34"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Robin David S\u00e9bastien Bardin Josselin Feist Laurent Mounier Marie-Laure Potet Thanh Dinh Ta and Jean-Yves Marion. 2016. Specification of concretization and symbolization policies in symbolic execution. In ISSTA. https:\/\/doi.org\/10.1145\/2931037.2931048 10.1145\/2931037.2931048","DOI":"10.1145\/2931037.2931048"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"Johan de Kleer. 1992. An Improved Incremental Algorithm for Generating Prime Implicates. In AAAI. https:\/\/doi.org\/10.1007\/978-3-642-60211-5_9 10.1007\/978-3-642-60211-5_9","DOI":"10.1007\/978-3-642-60211-5_9"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Isil Dillig and Thomas Dillig. 2013. Explain: A Tool for Performing Abductive Inference. In CAV. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_46 10.1007\/978-3-642-39799-8_46","DOI":"10.1007\/978-3-642-39799-8_46"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Isil Dillig Thomas Dillig Boyang Li and Ken McMillan. 2013. Inductive Invariant Generation via Abductive Inference. In OOPSLA. https:\/\/doi.org\/10.1145\/2509136.2509511 10.1145\/2509136.2509511","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"Adel Djoudi and S\u00e9bastien Bardin. 2015. BINSEC: Binary Code Analysis with Low-Level Regions. In TACAS. https: \/\/doi.org\/10.1007\/978-3-662-46681-0_17 10.1007\/978-3-662-46681-0_17","DOI":"10.1007\/978-3-662-46681-0_17"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","unstructured":"Louis Dureuil Guillaume Petiot Marie-Laure Potet Thanh-Ha Le Aude Crohen and Philippe de Choudens. 2016. FISSC: A Fault Injection and Simulation Secure Collection. In SAFECOMP. https:\/\/doi.org\/10.1007\/978-3-319-45477-1_1 10.1007\/978-3-319-45477-1_1","DOI":"10.1007\/978-3-319-45477-1_1"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"Mnacho Echenim Nicolas Peltier and Yanis Sellami. 2018. A Generic Framework for Implicate Generation Modulo Theories. In IJCAR. https:\/\/doi.org\/10.1007\/978-3-319-94205-6_19 10.1007\/978-3-319-94205-6_19","DOI":"10.1007\/978-3-319-94205-6_19"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"Mnacho Echenim Nicolas Peltier and Yanis Sellami. 2019. Ilinva: Using Abduction to Generate Loop Invariants. In FroCoS. https:\/\/doi.org\/10.1007\/978-3-030-29007-8_5 10.1007\/978-3-030-29007-8_5","DOI":"10.1007\/978-3-030-29007-8_5"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/3207692.3207711"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","unstructured":"Daniel Fremont Markus Rabe and Sanjit Seshia. 2017. Maximum Model Counting. Proceedings of the AAAI Conference on Artificial Intelligence (2017). https:\/\/doi.org\/10.1609\/aaai.v31i1.11138 10.1609\/aaai.v31i1.11138","DOI":"10.1609\/aaai.v31i1.11138"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Timon Gehr Dimitar Dimitrov and Martin Vechev. 2015. Learning Commutativity Specifications. In CAV. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_18 10.1007\/978-3-319-21690-4_18","DOI":"10.1007\/978-3-319-21690-4_18"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Guillaume Girol Benjamin Farinier and S\u00e9bastien Bardin. 2021. Not All Bugs Are Created Equal But Robust Reachability Can Tell the Difference. In CAV. https:\/\/doi.org\/10.1007\/978-3-030-81685-8_32 10.1007\/978-3-030-81685-8_32","DOI":"10.1007\/978-3-030-81685-8_32"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Guillaume Girol Benjamin Farinier and S\u00e9bastien Bardin. 2022. Introducing robust reachability. Formal Methods in System Design (2022). https:\/\/doi.org\/10.1007\/s10703-022-00402-x 10.1007\/s10703-022-00402-x","DOI":"10.1007\/s10703-022-00402-x"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Carla Gomes Ashish Sabharwal and Bart Selman. 2008. Model Counting. Frontiers in Artificial Intelligence and Applications (2008). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-633 10.3233\/978-1-58603-929-5-633","DOI":"10.3233\/978-1-58603-929-5-633"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Sumit Gulwani Saurabh Srivastava and Ramarathnam Venkatesan. 2008. Program Analysis as Constraint Solving. In PLDI. https:\/\/doi.org\/10.1145\/1379022.1375616 10.1145\/1379022.1375616","DOI":"10.1145\/1379022.1375616"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Max Hoffmann Falk Schellenberg and Christof Paar. 2021. ARMORY: Fully Automated and Exhaustive Fault Simulation on ARM-M Binaries. IEEE Transactions on Information Forensics and Security (2021). https:\/\/doi.org\/10.1109\/TIFS.2020.3027143 10.1109\/TIFS.2020.3027143","DOI":"10.1109\/TIFS.2020.3027143"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530128"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Seonmo Kim and Stephen McCamant. 2018. Bit-Vector Model Counting Using Statistical Estimation. https:\/\/doi.org\/10.1007\/978-3-319-89960-2_8 10.1007\/978-3-319-89960-2_8","DOI":"10.1007\/978-3-319-89960-2_8"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Patrick Koopmann Warren Del-Pinto Sophie Tourret and Renate A. Schmidt. 2020. Signature-Based Abduction for Expressive Description Logics. In KR. https:\/\/doi.org\/10.24963\/kr.2020\/59 10.24963\/kr.2020\/59","DOI":"10.24963\/kr.2020\/59"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","unstructured":"Jean-Marie Lagniez and Pierre Marquis. 2019. A Recursive Algorithm for Projected Model Counting. Proceedings of the AAAI Conference on Artificial Intelligence (2019). https:\/\/doi.org\/10.1609\/aaai.v33i01.33011536 10.1609\/aaai.v33i01.33011536","DOI":"10.1609\/aaai.v33i01.33011536"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","unstructured":"Pierre Marquis. 1991. Extending abduction from propositional to first-order logic. In Fundamentals of Artificial Intelligence Research. https:\/\/doi.org\/10.1007\/3-540-54507-7_12 10.1007\/3-540-54507-7_12","DOI":"10.1007\/3-540-54507-7_12"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","unstructured":"Andrew Matusiewicz Neil V. Murray and Erik Rosenthal. 2011. Tri-Based Set Operations and Selective Computation of Prime Implicates. In ISMIS. https:\/\/doi.org\/10.1007\/978-3-642-21916-0_23 10.1007\/978-3-642-21916-0_23","DOI":"10.1007\/978-3-642-21916-0_23"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Gr\u00e9goire Menguy S\u00e9bastien Bardin Nadjib Lazaar and Arnaud Gotlieb. 2022. Automated Program Analysis: Revisiting Precondition Inference through Constraint Acquisition. In IJCAI. https:\/\/doi.org\/10.24963\/ijcai.2022\/260 10.24963\/ijcai.2022\/260","DOI":"10.24963\/ijcai.2022\/260"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908099"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"Alessandro Previti Alexey Ignatiev Ant\u00f3nio Morgado and Joao Marques-Silva. 2015. Prime Compilation of Non-Clausal Formulae. In IJCAI. https:\/\/doi.org\/10.5555\/2832415.2832524 10.5555\/2832415.2832524","DOI":"10.5555\/2832415.2832524"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"Andrew Reynolds Haniel Barbosa Daniel Larraz and Cesare Tinelli. 2020. Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. In Automated Reasoning. https:\/\/doi.org\/10.1007\/978-3-030-51074-9_9 10.1007\/978-3-030-51074-9_9","DOI":"10.1007\/978-3-030-51074-9_9"},{"key":"e_1_3_1_44_1","doi-asserted-by":"crossref","unstructured":"Caterina Urban and Antoine Min\u00e9. 2015. Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation. In VMCAI.","DOI":"10.1007\/978-3-662-46081-8_11"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","unstructured":"Bilgiday Yuce Patrick Schaumont and Marc Witteman. 2018. Fault Attacks on Secure Embedded Software: Threats Design and Evaluation. Journal of Hardware and Systems Security (2018). https:\/\/doi.org\/10.1007\/s41635-018-0038-1 10.1007\/s41635-018-0038-1","DOI":"10.1007\/s41635-018-0038-1"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","unstructured":"Zhe Zhou Robert Dickerson Benjamin Delaware and Suresh Jagannathan. 2021. Data-Driven Abductive Inference of Library Specifications. In OOPSLA. https:\/\/doi.org\/10.1145\/3485493 10.1145\/3485493","DOI":"10.1145\/3485493"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632933","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632933","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:03:47Z","timestamp":1751659427000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632933"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":45,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632933"],"URL":"https:\/\/doi.org\/10.1145\/3632933","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}