{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:14:54Z","timestamp":1761920094123,"version":"build-2065373602"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,12,31]]},"abstract":"<jats:p>\n                    The B method is a formal method supported by a variety of tools. Those tools, like any complex piece of software, may suffer from performance issues and vulnerabilities. In this work, we leverage performance fuzzing to generate inputs that uncover potential performance issues in the\n                    <jats:sc>ProB<\/jats:sc>\n                    model checker and its employed constraint solving backends. These backends include a mix of constraint solvers that are directly implemented in\n                    <jats:sc>ProB<\/jats:sc>\n                    or are bindings to third-party solvers such as Z3. During constraint solving, any such backend can be selected to solve a given constraint. As performance fuzzing algorithm, we utilise BanditFuzz. BanditFuzz utilises two multi-armed bandit agents to control a fuzz generator and mutator. This way, the algorithm can generate targeted input benchmarks that are well-formed inputs to\n                    <jats:sc>ProB<\/jats:sc>\n                    yet exhibit significant performance differences between the employed constraint solvers. We describe how we adapted BanditFuzz for the B method, what differences exist to the original implementation for the SMT-LIB standard, and how we ensure well-definedness of the randomly generated benchmarks. Further, we consider two opposed approaches to integrate BanditFuzz with\n                    <jats:sc>ProB<\/jats:sc>\n                    : as an external tool that considers\n                    <jats:sc>ProB<\/jats:sc>\n                    as a black box, and as an internal tool that has direct dependency onto\n                    <jats:sc>ProB<\/jats:sc>\n                    \u2019s source code and can capitalise on available, internal functionalities. Our experiments successfully uncovered performance issues in specific backends and even external tooling, providing valuable insights into areas that required improvement. Ultimately, we conclude that BanditFuzz is a valuable tool for development and advocate for the external architecture, as its benefits outweigh the drawbacks.\n                  <\/jats:p>","DOI":"10.1145\/3715161","type":"journal-article","created":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T06:25:16Z","timestamp":1738304716000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Internal and External Performance Fuzzing of Well-Defined Constraints for the B Method"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0819-5554","authenticated-orcid":false,"given":"Jannik","family":"Dunkelau","sequence":"first","affiliation":[{"name":"Faculty of Mathematics and Natural Sciences, Institute of Computer Science, Heinrich Heine University D\u00fcsseldorf","place":["D\u00fcsseldorf, Germany"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[{"name":"Faculty of Mathematics and Natural Sciences, Institute of Computer Science, Heinrich Heine University D\u00fcsseldorf","place":["D\u00fcsseldorf, Germany"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,31]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45648-1_13"},{"key":"e_1_3_3_5_2","series-title":"Proceedings of Machine Learning Research","first-page":"39.1\u201339.26","volume-title":"25th Annual Conference on Learning Theory","volume":"23","author":"Agrawal Shipra","year":"2012","unstructured":"Shipra Agrawal and Navin Goyal. 2012. Analysis of Thompson sampling for the multi-armed bandit problem. In 25th Annual Conference on Learning Theory(Proceedings of Machine Learning Research, Vol. 23). PMLR, 39.1\u201339.26."},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90005-2"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_3_9_2","volume-title":"8th International Workshop on Satisfiability Modulo Theories","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB standard: Version 2.0. In 8th International Workshop on Satisfiability Modulo Theories."},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134020"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_8"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000482"},{"key":"e_1_3_3_13_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BFb0033845","volume-title":"Programming Languages: Implementations, Logics, and Programs","author":"Carlsson Mats","year":"1997","unstructured":"Mats Carlsson, Greger Ottosson, and Bj\u00f6rn Carlson. 1997. An open-ended finite domain constraint solver. In Programming Languages: Implementations, Logics, and Programs(LNCS, Vol. 1292). Springer, 191\u2013206."},{"key":"e_1_3_3_14_2","volume-title":"SICStus Prolog User\u2019s Manual","author":"Carlsson Mats","year":"1988","unstructured":"Mats Carlsson, Johan Widen, Johan Andersson, Stefan Andersson, Kent Boortz, Hans Nilsson, and Thomas Sj\u00f6land. 1988. SICStus Prolog User\u2019s Manual. Vol. 3. Swedish Institute of Computer Science, Kista, Sweden."},{"key":"e_1_3_3_15_2","first-page":"2249","article-title":"An empirical evaluation of Thompson sampling","volume":"24","author":"Chapelle Olivier","year":"2011","unstructured":"Olivier Chapelle and Lihong Li. 2011. An empirical evaluation of Thompson sampling. Advan. Neural Inf. Process. Syst. 24 (2011), 2249\u20132257.","journal-title":"Advan. Neural Inf. Process. Syst."},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISSREW55968.2022.00055"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_18_2","series-title":"CEUR Workshop Proceedings","first-page":"83","volume-title":"OVERLAY 2021: Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis","volume":"2987","author":"Dunkelau Jannik","year":"2021","unstructured":"Jannik Dunkelau and Leo Baldus. 2021. Ranking model checking backends for automated selection via classification and regression learning. In OVERLAY 2021: Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis(CEUR Workshop Proceedings, Vol. 2987). 83\u201389. Retrieved from http:\/\/ceur-ws.org\/Vol-2987\/paper14.pdf"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_9"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-47705-8_13"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-48077-6_8"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_3_23_2","first-page":"125","volume-title":"European Symposium on Programming","author":"Filli\u00e2tre Jean-Christophe","year":"2013","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3\u2014Where programs meet provers. In European Symposium on Programming. Springer, 125\u2013128."},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1997.1504"},{"key":"e_1_3_3_25_2","volume-title":"Network and Distributed System Security Symposium (NDSS\u201908)","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid, Michael Y. Levin, and David Molnar. 2008. Automated whitebox fuzz testing. In Network and Distributed System Security Symposium (NDSS\u201908). Internet Society."},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICMLA.2011.144"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000299"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.240.2"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2019.00023"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","unstructured":"Philipp K\u00f6rner Jens Bendisposto Jannik Dunkelau Sebastian Krings and Michael Leuschel. 2020. Integrating formal specifications into applications: the ProB Java API. In Formal Methods in System Design. DOI:10.1007\/s10703-020-00351-3","DOI":"10.1007\/s10703-020-00351-3"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_23"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3364452.3364455"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213861"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63461-2_4"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781119002727.ch14"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2018.2834476"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2946563"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/96267.96279"},{"key":"e_1_3_3_42_2","article-title":"Bitwuzla at the SMT-COMP 2020","volume":"2006","author":"Niemetz Aina","year":"2020","unstructured":"Aina Niemetz and Mathias Preiner. 2020. Bitwuzla at the SMT-COMP 2020. CoRR abs\/2006.01621 (May2020).","journal-title":"CoRR"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134073"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_31"},{"key":"e_1_3_3_45_2","first-page":"861","volume-title":"23rd USENIX Security Symposium (USENIX Security\u201914)","author":"Rebert Alexandre","year":"2014","unstructured":"Alexandre Rebert, Sang Kil Cha, Thanassis Avgerinos, Jonathan Foote, David Warren, Gustavo Grieco, and David Brumley. 2014. Optimizing seed selection for fuzzing. In 23rd USENIX Security Symposium (USENIX Security\u201914). USENIX Association, 861\u2013875."},{"key":"e_1_3_3_46_2","first-page":"346","volume-title":"14th International Conference on Integrated Formal Methods","author":"Schmidt Joshua","year":"2018","unstructured":"Joshua Schmidt, Sebastian Krings, and Michael Leuschel. 2018. Repair and generation of formal models using synthesis. In 14th International Conference on Integrated Formal Methods. Springer, 346\u2013366."},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-85248-1_7"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-022-00682-y"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63618-0_5"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_16"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_6"},{"key":"e_1_3_3_52_2","volume-title":"Reinforcement Learning: An Introduction (2nd ed.)","author":"Sutton Richard S.","year":"2018","unstructured":"Richard S. Sutton and Andrew G. Barto. 2018. Reinforcement Learning: An Introduction (2nd ed.). MIT Press. Retrieved from http:\/\/incompleteideas.net\/book\/the-book-2nd.html"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00992698"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380396"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2022.3168373"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3715161","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:07:34Z","timestamp":1761919654000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3715161"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,31]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12,31]]}},"alternative-id":["10.1145\/3715161"],"URL":"https:\/\/doi.org\/10.1145\/3715161","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2025,10,31]]},"assertion":[{"value":"2024-08-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-22","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-31","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}