{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,7]],"date-time":"2024-08-07T03:41:08Z","timestamp":1723002068166},"reference-count":69,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T00:00:00Z","timestamp":1591488000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T00:00:00Z","timestamp":1591488000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,10]]},"DOI":"10.1007\/s10009-020-00577-w","type":"journal-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T09:02:36Z","timestamp":1591520556000},"page":"601-615","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A study of learning likely data structure properties using machine learning models"],"prefix":"10.1007","volume":"22","author":[{"given":"Muhammad","family":"Usman","sequence":"first","affiliation":[]},{"given":"Wenxi","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Kaiyuan","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Cagdas","family":"Yelen","sequence":"additional","affiliation":[]},{"given":"Nima","family":"Dini","sequence":"additional","affiliation":[]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,6,7]]},"reference":[{"issue":"3","key":"577_CR1","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1080\/00031305.1992.10475879","volume":"46","author":"NS Altman","year":"1992","unstructured":"Altman, N.S.: An introduction to kernel and nearest-neighbor nonparametric regression. Am. Stat. 46(3), 175\u2013185 (1992)","journal-title":"Am. Stat."},{"key":"577_CR2","doi-asserted-by":"crossref","unstructured":"Baca\u00ebr, N.: Verhulst and the logistic equation 01, 1838 (2011)","DOI":"10.1007\/978-0-85729-115-8_6"},{"key":"577_CR3","doi-asserted-by":"crossref","unstructured":"Bodik, R.: Program synthesis: opportunities for the next decade. In: International Conference on Functional Programming, pp. 1\u20131 (2015)","DOI":"10.1145\/2784731.2789052"},{"key":"577_CR4","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: International Symposium on Software Testing and Analysis, pp. 123\u2013133 (2002)","DOI":"10.1145\/566171.566191"},{"key":"577_CR5","doi-asserted-by":"crossref","unstructured":"Briand, L.C., Labiche, Y., Liu, X.: Using machine learning to support debugging with tarantula. In: International Symposium on Software Reliability, pp. 137\u2013146 (2007)","DOI":"10.1109\/ISSRE.2007.31"},{"key":"577_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-1939-6","volume-title":"Spectra of Graphs","author":"AE Brouwer","year":"2012","unstructured":"Brouwer, A.E., Haemers, W.H.: Spectra of Graphs. Springer, New York (2012)"},{"issue":"OOPSLA","key":"577_CR7","first-page":"94:1","volume":"1","author":"A \u00c7elik","year":"2017","unstructured":"\u00c7elik, A., Pai, S., Khurshid, S., Gligoric, M.: Bounded exhaustive test-input generation on GPUs. PACMPL 1(OOPSLA), 94:1\u201394:25 (2017)","journal-title":"PACMPL"},{"key":"577_CR8","doi-asserted-by":"crossref","unstructured":"Chen, Y.-F., Hong, C.-D., Lin, A.W., R\u00fcmmer, P.: Learning to prove safety over parameterised concurrent systems. In: Formal Methods in Computer Aided Design, pp. 76\u201383 (2017)","DOI":"10.23919\/FMCAD.2017.8102244"},{"key":"577_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: Design Automation Conference, pp. 368\u2013371 (2003)","DOI":"10.21236\/ADA461052"},{"issue":"3","key":"577_CR10","first-page":"273","volume":"20","author":"C Cortes","year":"1995","unstructured":"Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273\u2013297 (1995)","journal-title":"Mach. Learn."},{"key":"577_CR11","doi-asserted-by":"crossref","unstructured":"Csallner, C., Tillmann, N., Smaragdakis, Y.: DySy: Dynamic symbolic execution for invariant inference. In: International Conference on Software Engineering, pp. 281\u2013290 (2008)","DOI":"10.1145\/1368088.1368127"},{"key":"577_CR12","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: International Conference on Automated Deduction, pp. 378\u2013388 (2015)","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"577_CR13","doi-asserted-by":"crossref","unstructured":"Demsky, B., Rinard, M.C.: Automatic detection and repair of errors in data structures. In: Conference on Object-Oriented Programming Systems, Languages and Applications, pp. 78\u201395 (2003)","DOI":"10.1145\/949343.949314"},{"key":"577_CR14","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. In: International Conference on Object Oriented Programming Systems Languages and Applications, pp. 443\u2013456 (2013)","DOI":"10.1145\/2544173.2509511"},{"key":"577_CR15","doi-asserted-by":"crossref","unstructured":"Dini, N., Yelen, C., Alrmaih, Z., Kulkarni, A., Khurshid, S.: Korat-API: a framework to enhance korat to better support testing and reliability techniques. In: International Symposium on Applied Computing, pp. 1934\u20131943 (2018)","DOI":"10.1145\/3167132.3167339"},{"key":"577_CR16","doi-asserted-by":"crossref","unstructured":"Dini, N., Yelen, C., Gligoric, M., Khurshid, S.: Extension-aware automated testing based on imperative predicates. In: Conference on Software Testing, Validation and Verification, pp. 25\u201336 (2019)","DOI":"10.1109\/ICST.2019.00013"},{"key":"577_CR17","doi-asserted-by":"crossref","unstructured":"Dini, N., Yelen, C., Khurshid, S.: Optimizing parallel Korat using invalid ranges. In: International Symposium on Model Checking of Software, pp. 182\u2013191 (2017)","DOI":"10.1145\/3092282.3092293"},{"key":"577_CR18","doi-asserted-by":"crossref","unstructured":"Elkarablieh, B., Garcia, I., Suen, Y.L., Sarfraz, K.: Assertion-based repair of complex data structures. In: International Conference on Automated Software Engineering, pp. 64\u201373 (2007)","DOI":"10.1145\/1321631.1321643"},{"key":"577_CR19","doi-asserted-by":"crossref","unstructured":"Ernst, M.D., Czeisler, A., Griswold, W.G., Notkin, D.: Quickly detecting relevant program invariants. In: International Conference on Software Engineering, pp. 449\u2013458 (2000)","DOI":"10.1145\/337180.337240"},{"issue":"1\u20133","key":"577_CR20","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"577_CR21","unstructured":"Facundo, M., Degiovanni, R., Ponzio, P., Regis, G., Aguirre, N., Frias, M.F.: Training binary classifiers as data structure invariants. In: International Conference on Software Engineering, pp. 759\u2013770 (2019)"},{"issue":"1","key":"577_CR22","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1006\/jcss.1997.1504","volume":"55","author":"Y Freund","year":"1997","unstructured":"Freund, Y., Schapire, R.E.: A decision-theoretic generalization of on-line learning and an application to boosting. J. Comput. Syst. Sci. 55(1), 119\u2013139 (1997)","journal-title":"J. Comput. Syst. Sci."},{"issue":"5","key":"577_CR23","doi-asserted-by":"publisher","first-page":"1189","DOI":"10.1214\/aos\/1013203451","volume":"29","author":"JH Friedman","year":"2001","unstructured":"Friedman, J.H.: Greedy function approximation: A gradient boosting machine. Ann. Statist. 29(5), 1189\u20131232 (2001)","journal-title":"Ann. Statist."},{"key":"577_CR24","doi-asserted-by":"crossref","unstructured":"Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: Symposium on Principles of Programming Languages, pp. 499\u2013512 (2016)","DOI":"10.1145\/2914770.2837664"},{"key":"577_CR25","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using verisoft. In: Symposium on Principles of Programming Languages, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"577_CR26","unstructured":"Gomes, C.P., Sabharwal, A., Selman, B.: Model counting (2008)"},{"key":"577_CR27","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Dimensions in program synthesis. In: International Symposium on Principles and Practice of Declarative Programming, pp. 13\u201324 (2010)","DOI":"10.1145\/1836089.1836091"},{"key":"577_CR28","unstructured":"Guo, C., Berkhahn, F.: Entity embeddings of categorical variables. CoRR (2016). arXiv:1604.06737"},{"key":"577_CR29","doi-asserted-by":"crossref","unstructured":"Hernandez, J., Carrasco-Ochoa, J.A., Mart\u00ednez-Trinidad, J.F.: An empirical study of oversampling and undersampling for instance selection methods on imbalance datasets. In: Progress in Pattern Recognition, Image Analysis, Computer Vision, and Applications, pp. 262\u2013269. Springer (2013)","DOI":"10.1007\/978-3-642-41822-8_33"},{"key":"577_CR30","unstructured":"Ho, T.K.: Random decision forests. In: International Conference on Document Analysis and Recognition (1995)"},{"key":"577_CR31","doi-asserted-by":"crossref","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Invariant generation in vampire. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 60\u201364. Springer (2011)","DOI":"10.1007\/978-3-642-19835-9_7"},{"key":"577_CR32","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: International Symposium on Software Testing and Analysis, pp. 14\u201325 (2000)","DOI":"10.1145\/347636.383378"},{"key":"577_CR33","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: International Conference on Software Engineering, pp. 215\u2013224 (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"577_CR34","doi-asserted-by":"crossref","unstructured":"Jump, M., McKinley, K.S.: Dynamic shape analysis via degree metrics. In: International Symposium on Memory Management, pp. 119\u2013128 (2009)","DOI":"10.1145\/1542431.1542449"},{"key":"577_CR35","doi-asserted-by":"crossref","unstructured":"Kazemi, S.M., Poole, D.: Relnn: A deep neural model for relational learning (2017)","DOI":"10.1609\/aaai.v32i1.12111"},{"key":"577_CR36","doi-asserted-by":"crossref","unstructured":"Ke, Y., Stolee, K.T, Goues, C.L., Brun, Y.: Repairing programs with semantic code search (T). In: International Conference on Automated Software Engineering, pp. 295\u2013306 (2015)","DOI":"10.1109\/ASE.2015.60"},{"key":"577_CR37","unstructured":"Korat GitHub repository. https:\/\/github.com\/korattest\/korat"},{"issue":"8","key":"577_CR38","doi-asserted-by":"publisher","first-page":"870","DOI":"10.1109\/32.57624","volume":"16","author":"B Korel","year":"1990","unstructured":"Korel, B.: Automated software test data generation. Trans. Softw. Eng. 16(8), 870\u2013879 (1990)","journal-title":"Trans. Softw. Eng."},{"key":"577_CR39","volume-title":"Program Development in Java-Abstraction, Specification, and Object-Oriented Design","author":"B Liskov","year":"2001","unstructured":"Liskov, B., Guttag, J.V.: Program Development in Java-Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, Boston (2001)"},{"key":"577_CR40","doi-asserted-by":"crossref","unstructured":"Malik, M., Pervaiz, A., Uzuncaova, E., Khurshid, S.: Deryaft: A tool for generating representation invariants of structurally complex data. In: International Conference on Software Engineering, pp. 859\u2013862 (2008)","DOI":"10.1145\/1368088.1368223"},{"key":"577_CR41","doi-asserted-by":"crossref","unstructured":"Malik, M.Z.: Dynamic shape analysis of program heap using graph spectra: NIER track. In: International Conference on Software Engineering, pp. 952\u2013955 (2011)","DOI":"10.1145\/1985793.1985956"},{"issue":"1","key":"577_CR42","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90\u2013121 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"577_CR43","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 413\u2013427 (2008)","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"577_CR44","doi-asserted-by":"crossref","unstructured":"Mera, E., Lopez-Garc\u00eda, P., Hermenegildo, M.: Integrating software testing and run-time checking in an assertion verification framework. In: Logic Programming, pp. 281\u2013295. Springer (2009)","DOI":"10.1007\/978-3-642-02846-5_25"},{"key":"577_CR45","unstructured":"Meyer, B.: Class invariants: concepts, problems, solutions. CoRR (2016). arXiv:1608.07637"},{"key":"577_CR46","doi-asserted-by":"crossref","unstructured":"Misailovic, S., Milicevic, A., Petrovic, N., Khurshid, S., Marinov, D.: Parallel test generation and execution with Korat. In: Symposium on the Foundations of Software Engineering, pp. 135\u2013144 (2007)","DOI":"10.1145\/1287624.1287645"},{"key":"577_CR47","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Conference on Programming Language Design and Implementation, pp. 221\u2013231 (2001)","DOI":"10.1145\/381694.378851"},{"issue":"5","key":"577_CR48","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0925-2312(91)90023-5","volume":"2","author":"F Murtagh","year":"1991","unstructured":"Murtagh, F.: Multilayer perceptrons for classification and regression. Neurocomputing 2(5), 183\u2013197 (1991)","journal-title":"Neurocomputing"},{"key":"577_CR49","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: International Conference on Software Engineering, pp. 75\u201384 (2007)","DOI":"10.1109\/ICSE.2007.37"},{"key":"577_CR50","unstructured":"Provost, F.: Machine learning from imbalanced data sets 101. In: Proceedings of the AAAI Workshop on Imbalanced Data Sets, pp. 1\u20133 (2000)"},{"issue":"1","key":"577_CR51","first-page":"81","volume":"1","author":"JR Quinlan","year":"1986","unstructured":"Quinlan, J.R.: Induction of decision trees. Mach. Learn. 1(1), 81\u2013106 (1986)","journal-title":"Mach. Learn."},{"key":"577_CR52","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Symposium on Logic in Computer Science, pp. 55\u201374 (2002)"},{"key":"577_CR53","unstructured":"Rish, I.: An empirical study of the naive bayes classifier. In: IJCAI, pp. 3 (2001)"},{"issue":"3","key":"577_CR54","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1214\/aoms\/1177729586","volume":"22","author":"H Robbins","year":"1951","unstructured":"Robbins, H., Monro, S.: A stochastic approximation method. Ann. Math. Stat. 22(3), 400\u2013407 (1951)","journal-title":"Ann. Math. Stat."},{"key":"577_CR55","doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Symposium on Principles of Programming Languages, pp. 105\u2013118 (1999)","DOI":"10.1145\/292540.292552"},{"key":"577_CR56","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using gr\u00f6bner bases. In: Symposium on Principles of Programming Languages, pp. 318\u2013329 (2004)","DOI":"10.1145\/982962.964028"},{"key":"577_CR57","unstructured":"Scikit-Learn Library. https:\/\/scikit-learn.org\/stable\/. Accessed 18 Apr 2019"},{"key":"577_CR58","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Le, S.: Learning loop invariants for program verification. In: Conference on Neural Information Processing Systems, pp. 7762\u20137773 (2018)"},{"key":"577_CR59","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Le, S.: Learning loop invariants for program verification. In: Advances in Neural Information Processing Systems, pp. 7751\u20137762 (2018)"},{"key":"577_CR60","doi-asserted-by":"crossref","unstructured":"Siddiqui, J.H., Khurshid, S.: PKorat: Parallel generation of structurally complex test inputs. In: International Conference on Software Testing Verification and Validation, pp. 250\u2013259 (2009)","DOI":"10.1109\/ICST.2009.48"},{"key":"577_CR61","doi-asserted-by":"crossref","unstructured":"Singh, S., Zhang, M., Khurshid, S.: Learning guided enumerative synthesis for superoptimization. In: International Symposium on Model Checking of Software, p. 172\u2013192 (2019)","DOI":"10.1007\/978-3-030-30923-7_10"},{"key":"577_CR62","unstructured":"Solar-Lezama, A.: Program Synthesis by Sketching. PhD thesis (2008)"},{"key":"577_CR63","doi-asserted-by":"crossref","unstructured":"Usman, M., Wang, W., Vasic, M., Wang, K., Vikalo, H., Khurshid, S.: A study of the learnability of relational properties. In: 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). To appear(2020)","DOI":"10.1145\/3385412.3386015"},{"key":"577_CR64","doi-asserted-by":"crossref","unstructured":"Usman, M., Wang, W., Wang, K., Yelen, C., Dini, N., Khurshid, S.: A study of learning data structure invariants using off-the-shelf tools. In: International Symposium on Model Checking of Software, pp. 226\u2013243 (2019)","DOI":"10.1007\/978-3-030-30923-7_13"},{"key":"577_CR65","doi-asserted-by":"crossref","unstructured":"Valiant, L.G.: A theory of the learnable. CACM 27(11) (1984)","DOI":"10.1145\/1968.1972"},{"key":"577_CR66","doi-asserted-by":"publisher","unstructured":"Vapnik, V.N., Chervonenkis, A.Ya.: On the uniform convergence of relative frequencies of events to their probabilities. In: Measures of Complexity: Festschrift for Alexey Chervonenkis. Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21852-6_3","DOI":"10.1007\/978-3-319-21852-6_3"},{"key":"577_CR67","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S.: Model checking programs. In: International Conference on Automated Software Engineering, pp. 3\u201312 (2000)","DOI":"10.1109\/ASE.2000.873645"},{"issue":"3","key":"577_CR68","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/0003-2670(96)00142-0","volume":"329","author":"W Wu","year":"1996","unstructured":"Wu, W., Mallet, Y., Walczak, B., Penninckx, W., Massart, D.L., Heuerding, S., Erni, F.: Comparison of regularized discriminant analysis linear discriminant analysis and quadratic discriminant analysis applied to nir data. Anal. Chim. Acta 329(3), 257\u2013265 (1996)","journal-title":"Anal. Chim. Acta"},{"key":"577_CR69","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: Conference on Programming Language Design and Implementation, pp. 349\u2013361 (2008)","DOI":"10.1145\/1379022.1375624"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00577-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00577-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00577-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,7]],"date-time":"2024-08-07T02:47:43Z","timestamp":1722998863000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00577-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,7]]},"references-count":69,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["577"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00577-w","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2020,6,7]]},"assertion":[{"value":"7 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}