{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T14:27:13Z","timestamp":1783348033218,"version":"3.54.6"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032306920","type":"print"},{"value":"9783032306937","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:00:00Z","timestamp":1782950400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:00:00Z","timestamp":1782950400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2027]]},"DOI":"10.1007\/978-3-032-30693-7_6","type":"book-chapter","created":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T14:08:32Z","timestamp":1783346912000},"page":"81-100","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Enhancing LLM-Based Proof Synthesis for\u00a0Rust Programs via\u00a0Semantic Chunking and\u00a0Hierarchical Context Expansion"],"prefix":"10.1007","author":[{"given":"Yuchen","family":"Zhang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cheng","family":"Wen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhiwu","family":"Xu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dugang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jialun","family":"Cao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuwei","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,2]]},"reference":[{"key":"6_CR1","unstructured":"Klabnik, S., Nichols, C.: The Rust programming language, No Starch Press (2023)"},{"issue":"POPL","key":"6_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158154","volume":"2","author":"R Jung","year":"2017","unstructured":"Jung, R., Jourdan, J.-H., Krebbers, R., Dreyer, D.: Rustbelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2(POPL), 1\u201334 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Xu, Z., Wu, B., Wen, C., Zhang, B., Qin, S., He, M.: RPG: rust library fuzzing with pool-based fuzz target generation and generic support. In: Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering, pp. 1\u201313 (2024)","DOI":"10.1145\/3597503.3639102"},{"issue":"OOPSLA1","key":"6_CR4","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1145\/3586037","volume":"7","author":"A Lattuada","year":"2023","unstructured":"Lattuada, A., et al.: Verus: verifying rust programs using linear ghost types. Proc. ACM Program. Lang. 7(OOPSLA1), 286\u2013315 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Lattuada, A., et al.: Verus: a practical foundation for systems verification. In: Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, pp. 438\u2013454 (2024)","DOI":"10.1145\/3694715.3695952"},{"key":"6_CR6","unstructured":"Aggarwal, P., Parno, B., Welleck, S.: Alphaverus: bootstrapping formally verified code generation through self-improving translation and treefinement. arXiv preprint arXiv:2412.06176 (2024)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Wen, C., et al.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: International Conference on Computer Aided Verification, pp. 302\u2013328. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-65630-9_16"},{"issue":"5","key":"6_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3744746","volume":"16","author":"H Naveed","year":"2025","unstructured":"Naveed, H., et al.: A comprehensive overview of large language models. ACM Trans. Intell. Syst. Technol. 16(5), 1\u201372 (2025)","journal-title":"ACM Trans. Intell. Syst. Technol."},{"key":"6_CR9","unstructured":"Wen, C., et al.: A survey on static code analysis with large language models. In: International Conference on Knowledge Science, Engineering and Management. Springer, Cham (2026)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Cao, J., et al.: From informal to formal\u2013incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs. In: Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 26984\u201327003 (2025)","DOI":"10.18653\/v1\/2025.acl-long.1310"},{"key":"6_CR11","unstructured":"Ma, Z., et al.: Towards practical requirement analysis and verification: a case study on software ip components in aerospace embedded systems. arXiv preprint arXiv:2404.00795 (2024)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Su, J., Deng, L., Wen, C., Qin, S., Tian, C.: CFSTRA: enhancing configurable program analysis through LLM-driven strategy selection based on code features. In: International Symposium on Theoretical Aspects of Software Engineering, pp. 374\u2013391. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-64626-3_22"},{"issue":"7","key":"6_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3653718","volume":"18","author":"C Wen","year":"2024","unstructured":"Wen, C., et al.: Automatically inspecting thousands of static bug warnings with large language model: How far are we? ACM Trans. Knowl. Discov. Data 18(7), 1\u201334 (2024)","journal-title":"ACM Trans. Knowl. Discov. Data"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Ma, Z., et al.: Automated LTL specification generation from industrial aerospace requirements. In: International Symposium on Formal Methods, pp. 1\u201320. Springer, Cham (2026)","DOI":"10.1007\/978-3-032-26220-2_33"},{"key":"6_CR15","unstructured":"Jiang, C., et al.: Large language models for multilingual code intelligence: a survey. In: International Conference on Knowledge Science, Engineering and Management. Springer, Cham (2026)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Lin, Y., et al.: How well does knowledge injection enhance LLM-aided formal protocol modeling? In: 2026 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER). IEEE (2026)","DOI":"10.1109\/SANER67736.2026.00103"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Wang, Y., et al.: Synergizing LLM-driven semantic reasoning with assertion-guided analysis for enhanced vulnerability detection. In: 2026 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER). IEEE (2026)","DOI":"10.1109\/SANER67736.2026.00075"},{"issue":"OOPSLA2","key":"6_CR18","doi-asserted-by":"publisher","first-page":"3454","DOI":"10.1145\/3763174","volume":"9","author":"C Yang","year":"2025","unstructured":"Yang, C., et al.: Autoverus: automated proof generation for rust code. Proc. ACM Program. Lang. 9(OOPSLA2), 3454\u20133482 (2025)","journal-title":"Proc. ACM Program. Lang."},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Zhang, S., Liu, H., Ma, Z., Liang, X., Wen, C.: Formal verification of aerospace software IP components: a multi-tool case study. In: Proceedings of the 2026 6th International Conference on Computer Network Security and Software Engineering, pp. 1\u20139 (2026)","DOI":"10.1145\/3803633.3803667"},{"key":"6_CR20","doi-asserted-by":"publisher","DOI":"10.1016\/j.inffus.2025.103466","volume":"125","author":"Z Ma","year":"2026","unstructured":"Ma, Z., Wen, C., Bin, Yu., Jie, S.: Integrating ensemble learning and large language models for efficient formal verification of IP-based aerospace systems. Inf. Fusion 125, 103466 (2026)","journal-title":"Inf. Fusion"},{"key":"6_CR21","unstructured":"Hu, J., et al.: When large language models meet formal theorem proving: a survey. In: International Conference on Knowledge Science, Engineering and Management. Springer, Cham (2026)"},{"key":"6_CR22","first-page":"9459","volume":"33","author":"P Lewis","year":"2020","unstructured":"Lewis, P., et al.: Retrieval-augmented generation for knowledge-intensive NLP tasks. Adv. Neural. Inf. Process. Syst. 33, 9459\u20139474 (2020)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"6_CR23","unstructured":"Gao, Y., et al.: Retrieval-augmented generation for large language models: a survey. arXiv preprint arXiv:2312.10997, 2(1), (2023)"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: CLO sed-loop verifiable code generation. In: International Symposium on AI Verification, pp. 134\u2013155. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Diffy: inductive reasoning of array programs using difference invariants. In: International Conference on Computer Aided Verification, pp. 911\u2013935. Springer, Cham (2021)","DOI":"10.1007\/978-3-030-81688-9_42"},{"issue":"FSE","key":"6_CR26","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1145\/3643763","volume":"1","author":"MRH Misu","year":"2024","unstructured":"Misu, M.R.H., Lopes, C.V., Ma, I., Noble, J.: Towards ai-assisted synthesis of verified Dafny methods. Proc. ACM Softw. Eng. 1(FSE), 812\u2013835 (2024)","journal-title":"Proc. ACM Softw. Eng."},{"key":"6_CR27","unstructured":"Zhong, S.C., Si, X.: Towards repository-level program verification with large language models. In: Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages, pp. 27\u201339 (2025)"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Ma, L., Liu, S., Li, Y., Xie, X., Bu, L.: Specgen: automated generation of formal program specifications via large language models. In: 2025 IEEE\/ACM 47th International Conference on Software Engineering (ICSE), pp. 16\u201328. IEEE (2025)","DOI":"10.1109\/ICSE55347.2025.00129"},{"key":"6_CR29","unstructured":"Chen, Z., et al.: Sld-spec: enhancement LLM-assisted specification generation for complex loop functions via program slicing and logical deletion. arXiv preprint arXiv:2509.09917arXiv preprint (2025)"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Liu, R., Chen, M., Wu, L-I., Ke, J., Li, G.: Enhancing automated loop invariant generation for complex programs with large language models. Sci. Comput. Program. 103387 (2025)","DOI":"10.1016\/j.scico.2025.103387"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Su, W., Wu, X., Zhao, Y.: NL2ACSL: interactively translating natural language to ANSI C specification language with large language models. Knowl. Based Syst. 115177 (2025)","DOI":"10.1016\/j.knosys.2025.115177"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., et al.: Ranking LLM-generated loop invariants for program verification. In: Findings of the Association for Computational Linguistics: EMNLP 2023, pp. 9164\u20139175 (2023)","DOI":"10.18653\/v1\/2023.findings-emnlp.614"},{"issue":"2","key":"6_CR33","first-page":"1","volume":"34","author":"J Li","year":"2025","unstructured":"Li, J., Li, G., Li, Y., Jin, Z.: Structured chain-of-thought prompting for code generation. ACM Trans. Softw. Eng. Methodol. 34(2), 1\u201323 (2025)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"6_CR34","unstructured":"Beg, A., O\u2019Donoghue, D., Monahan, R.: Evaluating LLM-generated ACSL annotations for formal verification. arXiv preprint arXiv:2602.13851 (2026)"},{"key":"6_CR35","doi-asserted-by":"publisher","first-page":"129120","DOI":"10.52202\/079017-4101","volume":"37","author":"C Liu","year":"2024","unstructured":"Liu, C., Xiwei, W., Feng, Y., Cao, Q., Yan, J.: Towards general loop invariant generation: a benchmark of programs with memory manipulation. Adv. Neural. Inf. Process. Syst. 37, 129120\u2013129145 (2024)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"6_CR36","unstructured":"Yan, C., et al.: Re: form\u2013reducing human priors in scalable formal software verification with RL in LLMs: a preliminary study on dafny. arXiv preprint arXiv:2507.16331 (2025)"},{"issue":"ISSTA","key":"6_CR37","doi-asserted-by":"publisher","first-page":"1009","DOI":"10.1145\/3728920","volume":"2","author":"W Cao","year":"2025","unstructured":"Cao, W., et al.: Clause2inv: a generate-combine-check framework for loop invariant inference. Proc. ACM Softw. Eng. 2(ISSTA), 1009\u20131030 (2025)","journal-title":"Proc. ACM Softw. Eng."},{"key":"6_CR38","unstructured":"Yang, C., Neamtu, N., Hawblitzel, C., Lorch, J.R., Lu, S.: Verusage: a study of agent-based verification for rust systems. arXiv preprint arXiv:2512.18436 (2025)"},{"key":"6_CR39","unstructured":"Sun, C., et al.: Veristruct: Ai-assisted automated verification of data-structure modules in verus. arXiv preprint arXiv:2510.25015 (2025)"},{"key":"6_CR40","unstructured":"Di, N., et al.: Reducing the costs of proof synthesis on rust systems by scaling up a seed training set. arXiv preprint arXiv:2602.04910 (2026)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-30693-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T14:09:38Z","timestamp":1783346978000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-30693-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,2]]},"ISBN":["9783032306920","9783032306937"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-30693-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,2]]},"assertion":[{"value":"2 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Shanghai","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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tase2026.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}