{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:13:22Z","timestamp":1760044402981},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030309220"},{"type":"electronic","value":"9783030309237"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30923-7_13","type":"book-chapter","created":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T23:04:08Z","timestamp":1569971048000},"page":"226-243","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Study of Learning Data Structure Invariants Using Off-the-shelf Tools"],"prefix":"10.1007","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":[[2019,10,2]]},"reference":[{"key":"13_CR1","unstructured":"Korat GitHub repository. https:\/\/github.com\/korattest\/korat"},{"key":"13_CR2","unstructured":"Scikit-Learn Library. https:\/\/scikit-learn.org\/stable\/ . Accessed 18 Aug 2019"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Bodik, R.: Program synthesis: opportunities for the next decade. In: 20th ACM SIGPLAN International Conference on Functional Programming, p. 1 (2015)","DOI":"10.1145\/2784731.2789052"},{"issue":"4","key":"13_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/566171.566191","volume":"27","author":"Chandrasekhar Boyapati","year":"2002","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 123\u2013133 (2002)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Briand, L.C., Labiche, Y., Liu, X.: Using machine learning to support debugging with tarantula. In: 18th IEEE International Symposium on Software Reliability, pp. 137\u2013146 (2007)","DOI":"10.1109\/ISSRE.2007.31"},{"key":"13_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). https:\/\/doi.org\/10.1007\/978-1-4614-1939-6"},{"key":"13_CR7","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 (FMCAD), pp. 76\u201383 (2017)","DOI":"10.23919\/FMCAD.2017.8102244"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: 40th Design Automation Conference, (DAC), pp. 368\u2013371 (2003)","DOI":"10.1145\/775925.775928"},{"issue":"3","key":"13_CR9","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":"13_CR10","doi-asserted-by":"crossref","unstructured":"Csallner, C., Tillmann, N., Smaragdakis, Y.: DySy: dynamic symbolic execution for invariant inference. In: 30th International Conference on Software Engineering, pp. 281\u2013290 (2008)","DOI":"10.1145\/1368088.1368127"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Demsky, B., Rinard, M.C.: Automatic detection and repair of errors in data structures. In: Proceedings of the 2003 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA, pp. 78\u201395 (2003)","DOI":"10.1145\/949343.949314"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. In: ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, pp. 443\u2013456 (2013)","DOI":"10.1145\/2544173.2509511"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Elkarablieh, B., Garcia, I., Suen, Y.L., Khurshid, S.: Assertion-based repair of complex data structures. In: IEEE\/ACM International Conference on Automated Software Engineering, pp. 64\u201373 (2007)","DOI":"10.1145\/1321631.1321643"},{"key":"13_CR14","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":"13_CR15","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., et al.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Molina, F., Degiovanni, R., Ponzio, P., Regis, G., Aguirre, N., Frias, M.F.: Training binary classifiers as data structure invariants. In: International Conference on Software Engineering (ICSE), May 2019","DOI":"10.1109\/ICSE.2019.00084"},{"issue":"1","key":"13_CR17","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":"13_CR18","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. Stat. 29(5), 1189\u20131232 (2001)","journal-title":"Ann. Stat."},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 499\u2013512 (2016)","DOI":"10.1145\/2914770.2837664"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Dimensions in program synthesis. In: 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, pp. 13\u201324 (2010)","DOI":"10.1145\/1836089.1836091"},{"key":"13_CR22","unstructured":"Ho, T.K.: Random decision forests. In: Third International Conference on Document Analysis and Recognition, vol. 1 (1995)"},{"key":"13_CR23","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2011","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2011)","edition":"1"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: International Symposium on Software Testing and Analysis (ISSTA), pp. 14\u201325 (2000)","DOI":"10.1145\/347636.383378"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: 32nd ACM\/IEEE International Conference on Software Engineering, vol. 1, pp. 215\u2013224 (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Jump, M., McKinley, K.S.: Dynamic shape analysis via degree metrics. In: 8th International Symposium on Memory Management (ISMM), pp. 119\u2013128 (2009)","DOI":"10.1145\/1542431.1542449"},{"issue":"8","key":"13_CR27","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. IEEE Trans. Softw. Eng. 16(8), 870\u2013879 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"13_CR28","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":"13_CR29","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: ACM\/IEEE 30th International Conference on Software Engineering (2008)","DOI":"10.1145\/1368088.1368223"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Malik, M.Z.: Dynamic shape analysis of program heap using graph spectra: NIER track. In: 33rd International Conference on Software Engineering (ICSE), pp. 952\u2013955 (2011)","DOI":"10.1145\/1985793.1985956"},{"issue":"1","key":"13_CR31","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":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413\u2013427. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_31"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-642-02846-5_25","volume-title":"Logic Programming","author":"E Mera","year":"2009","unstructured":"Mera, E., Lopez-Garc\u00eda, P., Hermenegildo, M.: Integrating software testing and run-time checking in an assertion verification framework. In: Hill, P.M., Warren, D.S. (eds.) ICLP 2009. LNCS, vol. 5649, pp. 281\u2013295. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02846-5_25"},{"key":"13_CR34","unstructured":"Meyer, B.: Class invariants: concepts, problems, solutions. CoRR, abs\/1608.07637 (2016)"},{"key":"13_CR35","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 221\u2013231 (2001)","DOI":"10.1145\/381694.378851"},{"issue":"5","key":"13_CR36","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":"13_CR37","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: 29th International Conference on Software Engineering, pp. 75\u201384 (2007)","DOI":"10.1109\/ICSE.2007.37"},{"key":"13_CR38","unstructured":"Provost, F.: Machine learning from imbalanced data sets 101. In: Proceedings of the AAAI 2000 Workshop on Imbalanced Data Sets, vol. 68, pp. 1\u20133. AAAI Press (2000)"},{"issue":"1","key":"13_CR39","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":"13_CR40","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science (2002)"},{"issue":"3","key":"13_CR41","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":"13_CR42","doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 105\u2013118 (1999)","DOI":"10.1145\/292540.292552"},{"key":"13_CR43","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using gr\u00f6bner bases. In: 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 318\u2013329 (2004)","DOI":"10.1145\/982962.964028"},{"key":"13_CR44","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems, vol. 31, pp. 7751\u20137762 (2018)"},{"key":"13_CR45","doi-asserted-by":"crossref","unstructured":"Singh, S., Zhang, M., Khurshid, S.: Learning guided enumerative synthesis for superoptimization (2019, under submission)","DOI":"10.1007\/978-3-030-30923-7_10"},{"key":"13_CR46","unstructured":"Solar-Lezama, A.: Program synthesis by sketching. Ph.D. thesis (2008)"},{"key":"13_CR47","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S.: Model checking programs. In: Fifteenth IEEE International Conference on Automated Software Engineering (ASE), pp. 3\u201312 (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"13_CR48","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 349\u2013361 (2008)","DOI":"10.1145\/1379022.1375624"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30923-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,8]],"date-time":"2019-12-08T14:55:44Z","timestamp":1575816944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30923-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309220","9783030309237"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30923-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"2 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/track\/spin-2019\/spin-2019-papers","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"13","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"45% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}