{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T20:00:07Z","timestamp":1769976007691,"version":"3.49.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,8,14]],"date-time":"2019-08-14T00:00:00Z","timestamp":1565740800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,8,14]],"date-time":"2019-08-14T00:00:00Z","timestamp":1565740800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004543","name":"China Scholarship Council","doi-asserted-by":"publisher","award":["201708060334"],"award-info":[{"award-number":["201708060334"]}],"id":[{"id":"10.13039\/501100004543","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2019,9,15]]},"DOI":"10.1007\/s10515-019-00264-4","type":"journal-article","created":{"date-parts":[[2019,8,14]],"date-time":"2019-08-14T17:02:40Z","timestamp":1565802160000},"page":"653-704","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Automatic B-model repair using model checking and machine learning"],"prefix":"10.1007","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6815-9091","authenticated-orcid":false,"given":"Cheng-Hao","family":"Cai","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1979-6622","authenticated-orcid":false,"given":"Jing","family":"Sun","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7245-0367","authenticated-orcid":false,"given":"Gillian","family":"Dobbie","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,14]]},"reference":[{"issue":"11","key":"264_CR1","doi-asserted-by":"publisher","first-page":"1780","DOI":"10.1016\/j.jss.2009.06.035","volume":"82","author":"R Abreu","year":"2009","unstructured":"Abreu, R., Zoeteweij, P., Golsteijn, R., van Gemund, A.J.C.: A practical evaluation of spectrum-based fault localization. J. Syst. Softw. 82(11), 1780\u20131792 (2009)","journal-title":"J. Syst. Softw."},{"key":"264_CR2","volume-title":"The B-book\u2014Assigning Programs to Meanings","author":"J Abrial","year":"2005","unstructured":"Abrial, J.: The B-book\u2014Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"issue":"6","key":"264_CR3","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J Abrial","year":"2010","unstructured":"Abrial, J., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"264_CR4","unstructured":"Alrajeh, D., Craven, R.: Automated error-detection and repair for compositional software specifications. In: 12th International Conference Software Engineering and Formal Methods, SEFM 2014, Grenoble, France, September 1\u20135, 2014. Proceedings, pp. 111\u2013127 (2014)"},{"key":"264_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"264_CR6","unstructured":"Babin, G., Ameur, Y.A., Singh, N.K., Pantel, M.: A system substitution mechanism for hybrid systems in Event-B. In: Proceedings 18th International Conference on Formal Engineering Methods Formal Methods and Software Engineering, ICFEM 2016, Tokyo, Japan, November 14\u201318, 2016, pp. 106\u2013121 (2016)"},{"key":"264_CR7","volume-title":"The Stanford Encyclopedia of Philosophy, winter 2017 edn.","author":"J Bagaria","year":"2017","unstructured":"Bagaria, J.: Set theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, winter 2017 edn. Stanford University, Stanford (2017)"},{"key":"264_CR8","unstructured":"Barbosa, H., D\u00e9harbe, D.: Formal verification of PLC programs using the B method. In: Abstract State Machines, Alloy, B, VDM, and Z\u2014Proceedings Third International Conference, ABZ 2012, Pisa, Italy, June 18\u201321, 2012, pp. 353\u2013356 (2012)"},{"key":"264_CR9","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.: M\u00e9t\u00e9or: A successful application of B in a large project. In: FM\u201999 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20\u201324, 1999, Proceedings, Volume I, pp. 369\u2013387 (1999)"},{"key":"264_CR10","unstructured":"Bena\u00efssa, N., Bonvoisin, D., Feliachi, A., Ordioni, J.: The PERF approach for formal verification. In: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification\u2014First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings, pp. 203\u2013214 (2016)"},{"key":"264_CR11","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-642-35289-8_25","volume-title":"Neural Networks: Tricks of the Trade","author":"L Bottou","year":"2012","unstructured":"Bottou, L.: Stochastic gradient descent tricks. In: Montavon, G. (ed.) Neural Networks: Tricks of the Trade, 2nd edn, pp. 421\u2013436. Springer, Berlin (2012)","edition":"2"},{"key":"264_CR12","doi-asserted-by":"publisher","unstructured":"Boulanger, J.L., Aljer, A., Mariano, G.: Formalization of digital circuits using the b method. WIT Trans. Built Environ. https:\/\/doi.org\/10.1002\/9781119002727.ch6 (2002)","DOI":"10.1002\/9781119002727.ch6"},{"key":"264_CR13","volume-title":"Classification and Regression Trees","author":"L Breiman","year":"1984","unstructured":"Breiman, L., Friedman, J.H., Olshen, R.A., Stone, C.J.: Classification and Regression Trees. Routledge, Wadsworth (1984)"},{"issue":"2","key":"264_CR14","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10\u201320 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"264_CR15","unstructured":"Cai, C., Sun, J., Dobbie, G.: B-repair: Repairing B-models using machine learning. In: 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12\u201314, 2018, pp. 31\u201340 (2018)"},{"key":"264_CR16","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: 11th International Conference Computer Aided Verification, CAV \u201999, Trento, Italy, July 6-10, 1999, Proceedings, pp. 495\u2013499 (1999)"},{"key":"264_CR17","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, pp. 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"264_CR18","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1111\/j.2517-6161.1958.tb00292.x","volume":"20","author":"DR Cox","year":"1958","unstructured":"Cox, D.R.: The regression analysis of binary sequences. J. R. Stat. Soc. Ser. B (Methodol.) 20, 215\u2013242 (1958)","journal-title":"J. R. Stat. Soc. Ser. B (Methodol.)"},{"issue":"7","key":"264_CR19","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. CAD Integrated Circuits Syst. 27(7), 1165\u20131178 (2008)","journal-title":"IEEE Trans. CAD Integrated Circuits Syst."},{"key":"264_CR20","unstructured":"Fadil, H., Koning, J.: A formal approach to model multiagent interactions using the B formal method. In: Advanced Distributed Systems: 5th International School and Symposium, ISSADS 2005, Guadalajara, Mexico, January 24\u201328, 2005, Revised Selected Papers, pp. 516\u2013528 (2005)"},{"issue":"1","key":"264_CR21","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/TSE.2017.2755013","volume":"45","author":"L Gazzola","year":"2019","unstructured":"Gazzola, L., Micucci, D., Mariani, L.: Automatic software repair: a survey. IEEE Trans. Softw. Eng. 45(1), 34\u201367 (2019)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"264_CR22","unstructured":"Glorot, X., Bordes, A., Bengio, Y.: Deep sparse rectifier neural networks. In: Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, AISTATS 2011, Fort Lauderdale, USA, April 11-13, 2011, pp. 315\u2013323 (2011)"},{"key":"264_CR23","unstructured":"Gopinath, D., Malik, M.Z., Khurshid, S.: Specification-based program repair using SAT. In: 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software Tools and Algorithms for the Construction and Analysis of Systems, ETAPS 2011, Saarbr\u00fccken, Germany, March 26\u2013April 3, 2011. Proceedings, pp. 173\u2013188 (2011)"},{"key":"264_CR24","first-page":"1","volume":"16","author":"D Harel","year":"2014","unstructured":"Harel, D., Katz, G., Marron, A., Weiss, G.: Non-intrusive repair of safety and liveness violations in reactive programs. Trans. Comput. Collective Intell. 16, 1\u201333 (2014)","journal-title":"Trans. Comput. Collective Intell."},{"key":"264_CR25","unstructured":"He, K., Zhang, X., Ren, S., Sun, J.: Deep residual learning for image recognition. In: 2016 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2016, Las Vegas, NV, USA, June 27\u201330, 2016, pp. 770\u2013778 (2016)"},{"key":"264_CR26","unstructured":"Ho, T.K.: Random decision forests. In: Third International Conference on Document Analysis and Recognition, ICDAR 1995, August 14\u201315, 1995, Montreal, Canada. Volume I, pp. 278\u2013282 (1995)"},{"key":"264_CR27","unstructured":"Hoffmann, S., Haugou, G., Gabriele, S., Burdy, L.: The b-method for the construction of microkernel-based systems. In: B 2007: Formal Specification and Development in B, 7th International Conference of B Users, Besan\u00e7on, France, January 17\u201319, 2007, Proceedings, pp. 257\u2013259 (2007)"},{"key":"264_CR28","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science\u2014Modelling and Reasoning About Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.D.: Logic in Computer Science\u2014Modelling and Reasoning About Systems, 2nd edn. Cambridge University Press, Cambridge (2004)","edition":"2"},{"key":"264_CR29","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering\u2014Volume 1, ICSE 2010, Cape Town, South Africa, 1-8 May 2010, pp. 215\u2013224 (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"264_CR30","unstructured":"Ke, Y., Stolee, K.T., Le Goues, C., Brun, Y.: Repairing programs with semantic code search (T). In: 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9-13, 2015, pp. 295\u2013306 (2015)"},{"key":"264_CR31","unstructured":"Krings, S., Leuschel, M.: SMT solvers for validation of B and Event-B models. In: Integrated Formal Methods\u201412th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings, pp. 361\u2013375 (2016)"},{"issue":"1","key":"264_CR32","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1016\/j.eswa.2006.09.004","volume":"34","author":"I Kurt","year":"2008","unstructured":"Kurt, I., Ture, M., Kurum, A.T.: Comparing performances of logistic regression, classification and regression tree, and neural networks for predicting coronary artery disease. Expert Syst. Appl. 34(1), 366\u2013374 (2008)","journal-title":"Expert Syst. Appl."},{"key":"264_CR33","unstructured":"Le, X.D., Chu, D., Lo, D., Le Goues, C., Visser, W.: S3: syntax- and semantic-guided repair synthesis via programming by examples. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2017, Paderborn, Germany, September 4\u20138, 2017, pp. 593\u2013604 (2017)"},{"key":"264_CR34","unstructured":"Le, X.D., Le, Q.L., Lo, D., Le Goues, C.: Enhancing automated program repair with deductive verification. In: 2016 IEEE International Conference on Software Maintenance and Evolution, ICSME 2016, Raleigh, NC, USA, October 2\u20137, 2016, pp. 428\u2013432 (2016a)"},{"key":"264_CR35","unstructured":"Le, X.D., Lo, D., Le Goues, C.: History driven program repair. In: IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering, SANER 2016, Suita, Osaka, Japan, March 14\u201318, 2016\u2014Volume 1, pp. 213\u2013224 (2016b)"},{"issue":"3","key":"264_CR36","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s11219-013-9208-0","volume":"21","author":"C Le Goues","year":"2013","unstructured":"Le Goues, C., Forrest, S., Weimer, W.: Current challenges in automatic software repair. Software Qual. J. 21(3), 421\u2013443 (2013)","journal-title":"Software Qual. J."},{"issue":"1","key":"264_CR37","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/TSE.2011.104","volume":"38","author":"C Le Goues","year":"2012","unstructured":"Le Goues, C., Nguyen, T., Forrest, S., Weimer, W.: Genprog: a generic method for automatic software repair. IEEE Trans. Softw. Eng. 38(1), 54\u201372 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"264_CR38","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transfer 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"264_CR39","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Cansell, D., Butler, M.J.: Validating and animating higher-order recursive functions in B. In: Rigorous Methods for Software Construction and Analysis, Essays Dedicated to Egon B\u00f6rger on the Occasion of His 60th Birthday, pp. 78\u201392 (2009)","DOI":"10.1007\/978-3-642-11447-2_6"},{"issue":"1","key":"264_CR40","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1002\/widm.8","volume":"1","author":"W Loh","year":"2011","unstructured":"Loh, W.: Classification and regression trees. Wiley Interdisc. Rew. Data Min. Knowl. Discov. 1(1), 14\u201323 (2011)","journal-title":"Wiley Interdisc. Rew. Data Min. Knowl. Discov."},{"key":"264_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Berlin (2002)"},{"key":"264_CR42","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October\u20131 November 1977, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"264_CR43","unstructured":"Schmidt, J., Krings, S., Leuschel, M.: Interactive model repair by synthesis. In: Abstract State Machines, Alloy, B, TLA, VDM, and Z\u20145th International Conference, ABZ 2016, Linz, Austria, May 23\u201327, 2016, Proceedings, pp. 303\u2013307 (2016)"},{"key":"264_CR44","unstructured":"Schmidt, J., Krings, S., Leuschel, M.: Repair and generation of formal models using synthesis. In: Integrated Formal Methods\u201414th International Conference, IFM 2018, Maynooth, Ireland, September 5\u20137, 2018, Proceedings, pp. 346\u2013366 (2018)"},{"issue":"3\/4","key":"264_CR45","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"JH Siekmann","year":"1989","unstructured":"Siekmann, J.H.: Unification theory. J. Symb. Comput. 7(3\/4), 207\u2013274 (1989)","journal-title":"J. Symb. Comput."},{"key":"264_CR46","unstructured":"Turian, J.P., Ratinov, L., Bengio, Y.: Word representations: a simple and general method for semi-supervised learning. In: ACL 2010, Proceedings of the 48th Annual Meeting of the Association for Computational Linguistics, July 11\u201316, 2010, Uppsala, Sweden, pp. 384\u2013394 (2010)"},{"key":"264_CR47","unstructured":"Wen, M., Chen, J., Wu, R., Hao, D., Cheung, S.: Context-aware patch generation for better automated program repair. In: Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27\u2013June 03, 2018, pp. 1\u201311 (2018)"},{"key":"264_CR48","unstructured":"Wilkerson, J.L., Tauritz, D.R.: Coevolutionary automated software correction. In: Genetic and Evolutionary Computation Conference, GECCO 2010, Proceedings, Portland, Oregon, USA, July 7\u201311, 2010, pp. 1391\u20131392 (2010)"},{"key":"264_CR49","unstructured":"Yang, G., Khurshid, S., Kim, M.: Specification-based test repair using a lightweight formal method. In: FM 2012: Formal Methods\u201418th International Symposium, Paris, France, August 27\u201331, 2012. Proceedings, pp. 455\u2013470 (2012)"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-019-00264-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-019-00264-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-019-00264-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,22]],"date-time":"2024-07-22T01:03:41Z","timestamp":1721610221000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-019-00264-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,14]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,9,15]]}},"alternative-id":["264"],"URL":"https:\/\/doi.org\/10.1007\/s10515-019-00264-4","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,8,14]]},"assertion":[{"value":"12 November 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 August 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 August 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}