{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:12Z","timestamp":1775873532246,"version":"3.50.1"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030532901","type":"print"},{"value":"9783030532918","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53291-8_9","type":"book-chapter","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:03:35Z","timestamp":1594843415000},"page":"151-164","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Code2Inv: A Deep Learning Framework for Program Verification"],"prefix":"10.1007","author":[{"given":"Xujie","family":"Si","sequence":"first","affiliation":[]},{"given":"Aaditya","family":"Naik","sequence":"additional","affiliation":[]},{"given":"Hanjun","family":"Dai","sequence":"additional","affiliation":[]},{"given":"Mayur","family":"Naik","sequence":"additional","affiliation":[]},{"given":"Le","family":"Song","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"key":"9_CR1","unstructured":"Allamanis, M., Brockschmidt, M., Khademi, M.: Learning to represent programs with graphs. In: Proceedings of the International Conference on Learning Representations (ICLR) (2018)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD) (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-662-54577-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2017","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 319\u2013336. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54577-5_18"},{"issue":"12","key":"9_CR4","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/3208071","volume":"61","author":"R Alur","year":"2018","unstructured":"Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun. ACM 61(12), 84\u201393 (2018)","journal-title":"Commun. ACM"},{"key":"9_CR5","unstructured":"Bahdanau, D., Cho, K., Bengio, Y.: Neural machine translation by jointly learning to align and translate. In: Proceedings of the International Conference on Learning Representations (ICLR) (2015)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"9_CR7","unstructured":"Chung, J., G\u00fcl\u00e7ehre, \u00c7., Cho, K., Bengio, Y.: Empirical evaluation of gated recurrent neural networks on sequence modeling. CoRR abs\/1412.3555 (2014)"},{"key":"9_CR8","unstructured":"Dai, H., Dai, B., Song, L.: Discriminative embeddings of latent variable models for structured data. In: Proceedings of the International Conference on Machine Learning (ICML) (2016)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE:\u00a0a\u00a0robust\u00a0framework\u00a0for\u00a0learning\u00a0invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_5"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: Proceedings of the ACM Symposium on Principles of Programming Languages (POPL) (2016)","DOI":"10.1145\/2837614.2837664"},{"key":"9_CR11","unstructured":"Gilmer, J., Schoenholz, S.S., Riley, P.F., Vinyals, O., Dahl, G.E.: Neural message passing for quantum chemistry. In: Proceedings of the International Conference on Machine Learning (ICML), pp. 1263\u20131272 (2017)"},{"key":"9_CR12","unstructured":"Graves, A., Wayne, G., Danihelka, I.: Neural turing machines. CoRR abs\/1410.5401 (2014)"},{"key":"9_CR13","unstructured":"Grefenstette, E., Hermann, K.M., Suleyman, M., Blunsom, P.: Learning to transduce with unbounded memory. In: Proceedings of the Conference on Neural Information Processing Systems (NIPS), pp. 1828\u20131836 (2015)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Heo, K., Raghothaman, M., Si, X., Naik, M.: Continuously reasoning about programs using differential Bayesian inference. In: Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI) (2019)","DOI":"10.1145\/3314221.3314616"},{"issue":"8","key":"9_CR16","doi-asserted-by":"publisher","first-page":"1735","DOI":"10.1162\/neco.1997.9.8.1735","volume":"9","author":"S Hochreiter","year":"1997","unstructured":"Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural Comput. 9(8), 1735\u20131780 (1997)","journal-title":"Neural Comput."},{"key":"9_CR17","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 (2010)","DOI":"10.1145\/1806799.1806833"},{"issue":"3","key":"9_CR18","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016)","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR19","unstructured":"Li, Y., Tarlow, D., Brockschmidt, M., Zemel, R.: Gated graph sequence neural networks. arXiv preprint \narXiv:1511.05493\n\n (2015)"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Logozzo, F., Lahiri, S.K., F\u00e4hndrich, M., Blackshear, S.: Verification modulo versions: towards usable verification. In: Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI) (2014)","DOI":"10.1145\/2594291.2594326"},{"key":"9_CR21","unstructured":"McMillan, K.L., Rybalchenko, A.: Solving constrained horn clauses using interpolation. Technical report MSR-TR-2013-6 (2013)"},{"issue":"7540","key":"9_CR22","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1038\/nature14236","volume":"518","author":"V Mnih","year":"2015","unstructured":"Mnih, V., et al.: Human-level control through deep reinforcement learning. Nature 518(7540), 529\u2013533 (2015)","journal-title":"Nature"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"GC Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213\u2013228. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45937-5_16"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.: Continuous reasoning: scaling the impact of formal methods. In: Proceedings of the Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS) (2018)","DOI":"10.1145\/3209108.3209109"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Padhi, S., Sharma, R., Millstein, T.: Data-driven precondition inference with learned features. In: Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI) (2016)","DOI":"10.1145\/2908080.2908099"},{"key":"9_CR27","unstructured":"Ryan, G., Wong, J., Yao, J., Gu, R., Jana, S.: CLN2INV: learning loop invariants with continuous logic networks. In: Proceedings of the International Conference on Learning Representations (ICLR) (2020)"},{"issue":"1","key":"9_CR28","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/TNN.2008.2005605","volume":"20","author":"F Scarselli","year":"2009","unstructured":"Scarselli, F., Gori, M., Tsoi, A.C., Hagenbuchner, M., Monfardini, G.: The graph neural network model. IEEE Trans. Neural Networks 20(1), 61\u201380 (2009)","journal-title":"IEEE Trans. Neural Networks"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-319-08867-9_6","volume-title":"Computer Aided Verification","author":"R Sharma","year":"2014","unstructured":"Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 88\u2013105. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_6"},{"key":"9_CR30","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. In: Proceedings of the Conference on Neural Information Processing Systems (NIPS) (2018)"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Saraswat, V., Seshia, S.: Combinatorial sketching for finite programs. In: Proceedings of Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: Proceedings of the ACM Symposium on Principles of Programming Languages (POPL) (2010)","DOI":"10.1145\/1706299.1706337"},{"key":"9_CR33","unstructured":"Sukhbaatar, S., Weston, J., Fergus, R., et al.: End-to-end memory networks. In: Proceedings of the Conference on Neural Information Processing Systems (NIPS) (2015)"},{"key":"9_CR34","doi-asserted-by":"publisher","DOI":"10.1109\/TNN.1998.712192","volume-title":"Reinforcement Learning - An Introduction","author":"RS Sutton","year":"1998","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning - An Introduction. MIT Press, Adaptive computation and machine learning (1998)"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Tai, K.S., Socher, R., Manning, C.D.: Improved semantic representations from tree-structured long short-term memory networks. In: Proceedings of the Association for Computational Linguistics (ACL) (2015)","DOI":"10.3115\/v1\/P15-1150"},{"key":"9_CR36","unstructured":"Xu, K., Hu, W., Leskovec, J., Jegelka, S.: How powerful are graph neural networks? In: Proceedings of the International Conference on Learning Representations (ICLR) (2019)"},{"key":"9_CR37","unstructured":"Ying, R., et al.: Hierarchical graph representation learning with differentiable pooling. In: Proceedings of the Conference on Neural Information Processing Systems (NIPS) (2018)"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Zhu, H., Magill, S., Jagannathan, S.: A data-driven CHC solver. In: Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI) (2018)","DOI":"10.1145\/3192366.3192416"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53291-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:05:07Z","timestamp":1594843507000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-53291-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030532901","9783030532918"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53291-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair.org","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"240","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":"43","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":"22","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":"18% - 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":"4","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":"11","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)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}