{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:53:28Z","timestamp":1782878008172,"version":"3.54.5"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T00:00:00Z","timestamp":1656547200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2022,6,30]]},"abstract":"<jats:p>Automated model repair techniques enable machines to synthesise patches that ensure models meet given requirements. B-repair, which is an existing model repair approach, assists users in repairing erroneous models in the B formal method, but repairing large models is inefficient due to successive applications of repair. In this work, we improve the performance of B-repair using simultaneous modifications, repair refactoring, and better classifiers. The simultaneous modifications can eliminate multiple invariant violations at a time so the average time to repair each fault can be reduced. Further, the modifications can be refactored to reduce the length of repair. The purpose of using better classifiers is to perform more accurate and general repairs and avoid inefficient brute-force searches. We conducted an empirical study to demonstrate that the improved implementation leads to the entire model process achieving higher accuracy, generality, and efficiency.<\/jats:p>","DOI":"10.1145\/3536430","type":"journal-article","created":{"date-parts":[[2022,5,14]],"date-time":"2022-05-14T13:09:57Z","timestamp":1652533797000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Fast Automated Abstract Machine Repair Using Simultaneous Modifications and Refactoring"],"prefix":"10.1145","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6815-9091","authenticated-orcid":false,"given":"Cheng-Hao","family":"Cai","sequence":"first","affiliation":[{"name":"School of Computer Science, University of Auckland, Auckland, New Zealand"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1979-6622","authenticated-orcid":false,"given":"Jing","family":"Sun","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Auckland, Auckland, New Zealand"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7245-0367","authenticated-orcid":false,"given":"Gillian","family":"Dobbie","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Auckland, Auckland, New Zealand"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7164-0580","authenticated-orcid":false,"given":"Zh\u00e9","family":"H\u00f3u","sequence":"additional","affiliation":[{"name":"Institute for Integrated and Intelligent Systems, Griffith University, Queensland, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3326-7855","authenticated-orcid":false,"given":"Hadrien","family":"Bride","sequence":"additional","affiliation":[{"name":"Institute for Integrated and Intelligent Systems, Griffith University, Queensland, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6512-8326","authenticated-orcid":false,"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[{"name":"School of Computing, National University of Singapore, Singapore and Institute for Integrated and Intelligent Systems, Griffith University, Queensland, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8457-3097","authenticated-orcid":false,"given":"Scott Uk-Jin","family":"Lee","sequence":"additional","affiliation":[{"name":"College of Computing, Hanyang University ERICA, Ansan, Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,9,20]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2009.06.035"},{"key":"e_1_3_2_3_2","volume-title":"The B-book - Assigning Programs to Meanings","author":"Abrial Jean-Raymond","year":"2005","unstructured":"Jean-Raymond Abrial. 2005. The B-book - Assigning Programs to Meanings. Cambridge University Press."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2001576.2001768"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/2658986"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30885-7_30"},{"key":"e_1_3_2_7_2","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/978-3-319-33951-1_15","volume-title":"Proceedings of the 1st International Conference on Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"Bena\u00efssa Nazim","year":"2016","unstructured":"Nazim Bena\u00efssa, David Bonvoisin, Abderrahmane Feliachi, and Julien Ordioni. 2016. The PERF approach for formal verification. In Proceedings of the 1st International Conference on Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. 203\u2013214."},{"key":"e_1_3_2_8_2","volume-title":"Pattern Recognition and Machine Learning, 5th Edition","author":"Bishop Christopher M.","year":"2007","unstructured":"Christopher M. Bishop. 2007. Pattern Recognition and Machine Learning, 5th Edition. Springer."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.eswa.2021.114806"},{"key":"e_1_3_2_10_2","first-page":"412","volume-title":"Proceedings of the 20th International Conference on Formal Engineering Methods (ICFEM\u201918)","author":"Bride Hadrien","year":"2018","unstructured":"Hadrien Bride, Jie Dong, Jin Song Dong, and Zh\u00e9 H\u00f3u. 2018. Towards dependable and explainable machine learning using automated reasoning. In Proceedings of the 20th International Conference on Formal Engineering Methods (ICFEM\u201918). 412\u2013416."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-019-00264-4"},{"key":"e_1_3_2_12_2","first-page":"1324","volume-title":"Proceedings of the 11th International Joint Conference on Artificial Intelligence (IJCAI\u201989)","author":"Kleer Johan de","year":"1989","unstructured":"Johan de Kleer and Brian C. Williams. 1989. Diagnosis with behavioral modes. In Proceedings of the 11th International Joint Conference on Artificial Intelligence (IJCAI\u201989). 1324\u20131330."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.patrec.2005.10.010"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2755013"},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1109\/ICDAR.1995.598994","volume-title":"Proceedings of the 3rd International Conference on Document Analysis and Recognition (ICDAR\u201995)","author":"Ho Tin Kam","year":"1995","unstructured":"Tin Kam Ho. 1995. Random decision forests. In Proceedings of the 3rd International Conference on Document Analysis and Recognition (ICDAR\u201995). 278\u2013282."},{"key":"e_1_3_2_16_2","first-page":"257","volume-title":"Proceedings of the 7th International Conference of B Users","author":"Hoffmann Sarah","year":"2007","unstructured":"Sarah Hoffmann, Germain Haugou, Sophie Gabriele, and Lilian Burdy. 2007. The B-method for the construction of microkernel-based systems. In Proceedings of the 7th International Conference of B Users. 257\u2013259."},{"key":"e_1_3_2_17_2","first-page":"197","volume-title":"Proceedings of the 40th IEEE Annual Computer Software and Applications Conference (COMPSAC\u201916)","author":"Ji Tao","year":"2016","unstructured":"Tao Ji, Liqian Chen, Xiaoguang Mao, and Xin Yi. 2016. Automated program repair by using similar code containing fix ingredients. In Proceedings of the 40th IEEE Annual Computer Software and Applications Conference (COMPSAC\u201916). 197\u2013202."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.60"},{"key":"e_1_3_2_19_2","first-page":"50","volume-title":"Proceedings of the 3rd International Workshop on Approaches and Applications of Inductive Programming","author":"Kitzelmann Emanuel","year":"2009","unstructured":"Emanuel Kitzelmann. 2009. Inductive programming: A survey of program synthesis techniques. In Proceedings of the 3rd International Workshop on Approaches and Applications of Inductive Programming. 50\u201373."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-48077-6_22"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227211"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.104"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-48077-6_27"},{"key":"e_1_3_2_25_2","first-page":"166","volume-title":"Proceedings of the 10th Joint Meeting on Foundations of Software Engineering","author":"Long Fan","year":"2015","unstructured":"Fan Long and Martin Rinard. 2015. Staged program repair with condition synthesis. In Proceedings of the 10th Joint Meeting on Foundations of Software Engineering. 166\u2013178."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1953048.2078195"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2312918"},{"key":"e_1_3_2_28_2","first-page":"1053","volume-title":"Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI)","author":"Pill Ingo","year":"2013","unstructured":"Ingo Pill and Thomas Quaritsch. 2013. Behavioral diagnosis of LTL specifications at operator level. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI). 1053\u20131059."},{"key":"e_1_3_2_29_2","first-page":"254","volume-title":"Proceedings of the 36th International Conference on Software Engineering (ICSE\u201914)","author":"Qi Yuhua","year":"2014","unstructured":"Yuhua Qi, Xiaoguang Mao, Yan Lei, Ziying Dai, and Chengsong Wang. 2014. The strength of random search on automated program repair. In Proceedings of the 36th International Conference on Software Engineering (ICSE\u201914). 254\u2013265."},{"key":"e_1_3_2_30_2","volume-title":"Artificial Intelligence - A Modern Approach","author":"Russell Stuart J.","year":"2010","unstructured":"Stuart J. Russell and Peter Norvig. 2010. Artificial Intelligence - A Modern Approach (3rd International ed.). Pearson Education."},{"key":"e_1_3_2_31_2","volume-title":"Reading between the Packets\u2014Implicit Feedback in Wireless Multihop Networks","author":"Scheuermann Bj\u00f6rn","year":"2007","unstructured":"Bj\u00f6rn Scheuermann. 2007. Reading between the Packets\u2014Implicit Feedback in Wireless Multihop Networks. Ph. D. Dissertation. University of D\u00fcsseldorf, Germany."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.adhoc.2007.01.001"},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/978-3-319-33600-8_25","volume-title":"Proceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"Schmidt Joshua","year":"2016","unstructured":"Joshua Schmidt, Sebastian Krings, and Michael Leuschel. 2016. Interactive model repair by synthesis. In Proceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z. 303\u2013307."},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/978-3-319-98938-9_20","volume-title":"Proceedings of the 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 Proceedings of the 14th International Conference on Integrated Formal Methods. 346\u2013366."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/IAS.2007.23"},{"key":"e_1_3_2_36_2","first-page":"384","volume-title":"Proceedings of the 48th Annual Meeting of the Association for Computational Linguistics (ACL)","author":"Turian Joseph P.","year":"2010","unstructured":"Joseph P. Turian, Lev-Arie Ratinov, and Yoshua Bengio. 2010. Word representations: A simple and general method for semi-supervised learning. In Proceedings of the 48th Annual Meeting of the Association for Computational Linguistics (ACL). 384\u2013394."},{"key":"e_1_3_2_37_2","first-page":"4644","volume-title":"Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI\u201921)","author":"Wang Shoujin","year":"2021","unstructured":"Shoujin Wang, Liang Hu, Yan Wang, Xiangnan He, Quan Z. Sheng, Mehmet A. Orgun, Longbing Cao, Francesco Ricci, and Philip S. Yu. 2021. Graph learning based recommender systems: A review. In Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI\u201921). 4644\u20134652."},{"key":"e_1_3_2_38_2","first-page":"1391","volume-title":"Proceedings of the Genetic and Evolutionary Computation Conference (GECCO\u201910)","author":"Wilkerson Josh L.","year":"2010","unstructured":"Josh L. Wilkerson and Daniel R. Tauritz. 2010. Coevolutionary automated software correction. In Proceedings of the Genetic and Evolutionary Computation Conference (GECCO\u201910). 1391\u20131392."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3536430","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3536430","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:50Z","timestamp":1750186970000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3536430"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,30]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,6,30]]}},"alternative-id":["10.1145\/3536430"],"URL":"https:\/\/doi.org\/10.1145\/3536430","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,6,30]]},"assertion":[{"value":"2020-02-21","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-05-05","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-09-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}