{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:58:56Z","timestamp":1782867536281,"version":"3.54.5"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-22749-2_6","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:12:27Z","timestamp":1776258747000},"page":"109-128","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-9226-3688","authenticated-orcid":false,"given":"Chuyue","family":"Sun","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0370-1676","authenticated-orcid":false,"given":"Yican","family":"Sun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0954-7881","authenticated-orcid":false,"given":"Daneshvar","family":"Amrollahi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ethan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4446-4777","authenticated-orcid":false,"given":"Shuvendu","family":"Lahiri","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0757-4600","authenticated-orcid":false,"given":"Shan","family":"Lu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6189-0866","authenticated-orcid":false,"given":"David","family":"Dill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"6_CR1","unstructured":"Artifact of veristruct (2025), https:\/\/github.com\/ChuyueSun\/VeriStruct"},{"key":"6_CR2","unstructured":"Anthropic: Claude code. https:\/\/claude.ai\/claude-code (2025), accessed: 2025"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Barrett, C., Boyd, B., Bursztein, E., Carlini, N., Chen, B., Choi, J., Chowdhury, A.R., Christodorescu, M., Datta, A., Feizi, S., Fisher, K., Hashimoto, T., Hendrycks, D., Jha, S., Kang, D., Kerschbaum, F., Mitchell, E., Mitchell, J., Ramzan, Z., Shams, K., Song, D., Taly, A., Yang, D.: Identifying and mitigating the security risks of generative ai. Foundations and Trends in Privacy and Security 6(1), 1\u201352 (2023). https:\/\/doi.org\/10.1561\/3300000041, https:\/\/doi.org\/10.1561\/3300000041","DOI":"10.1561\/3300000041"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, chap.\u00a033, pp. 825\u2013885. IOS Press (Feb 2021), http:\/\/theory.stanford.edu\/~barrett\/pubs\/BSST21.pdf","DOI":"10.3233\/FAIA201017"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) Proceedings of the 10th International Conference on Software Engineering and Formal Methods (SEFM 2012). Lecture Notes in Computer Science, vol.\u00a07504, pp. 233\u2013247. Springer, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"6_CR6","unstructured":"Dong, Q., Li, L., Dai, D., Zheng, C., Ma, J., Li, R., Xia, H., Xu, J., Wu, Z., Liu, T., et\u00a0al.: A survey on in-context learning. arXiv preprint arXiv:2301.00234 (2022)"},{"key":"6_CR7","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3. https:\/\/why3.lri.fr (2024), version 1.6.0"},{"key":"6_CR8","unstructured":"Fu, Y., Baker, E., Ding, Y., Chen, Y.: Constrained decoding for secure code generation. arXiv preprint arXiv:2405.00218 (2024)"},{"key":"6_CR9","unstructured":"Kamath, A., Senthilnathan, A., Chakraborty, S., Deligiannis, P., Lahiri, S.K., Lal, A., Rastogi, A., Roy, S., Sharma, R.: Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948 (2023)"},{"key":"6_CR10","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 1: Fundamental Algorithms. Addison-Wesley (1997)"},{"key":"6_CR11","unstructured":"Lahiri, S.K.: Evaluating llm-driven user-intent formalization for verification-aware languages. In: CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN\u2013FMCAD 2024. p.\u00a0142 (2024)"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Lattuada, A., Hance, T., Bosamiya, J., Brun, M., Cho, C., LeBlanc, H., Srinivasan, P., Achermann, R., Chajed, T., Hawblitzel, C., Howell, J., Lorch, J.R., Padon, O., Parno, B.: Verus: A practical foundation for systems verification. In: Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles. p. 438\u2013454. SOSP \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3694715.3695952, https:\/\/doi.org\/10.1145\/3694715.3695952","DOI":"10.1145\/3694715.3695952"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Lattuada, A., Hance, T., Cho, C., Brun, M., Subasinghe, I., Zhou, Y., Howell, J., Parno, B., Hawblitzel, C.: Verus: Verifying Rust programs using linear ghost types. Proceedings of the ACM on Programming Languages (2023). https:\/\/doi.org\/10.1145\/3586037","DOI":"10.1145\/3586037"},{"key":"6_CR14","unstructured":"Lattuada, A., Parno, B., Bosamiya, J., Hawblitzel, C., Hance, T., et\u00a0al.: vstd: Verus standard library. https:\/\/github.com\/verus-lang\/verus\/tree\/main\/vstd (Jun 2024), version 0.0.0, MIT License"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2010). Lecture Notes in Computer Science, vol.\u00a06355, pp. 348\u2013370. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Levy, A., Campbell, B., Ghena, B., Giffin, D.B., Pannuto, P., Dutta, P., Levis, P.: Multiprogramming a 64kb computer safely and efficiently. In: Proceedings of the 26th Symposium on Operating Systems Principles. p. 234\u2013251. SOSP \u201917, Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3132747.3132786, https:\/\/doi.org\/10.1145\/3132747.3132786","DOI":"10.1145\/3132747.3132786"},{"key":"6_CR17","unstructured":"Lewis, P., Perez, E., Piktus, A., Petroni, F., Karpukhin, V., Goyal, N., K\u00fcttler, H., Lewis, M., Yih, W.t., Rockt\u00e4schel, T., Riedel, S., Kiela, D.: Retrieval-augmented generation for knowledge-intensive nlp tasks. In: Proceedings of the 34th International Conference on Neural Information Processing Systems. NIPS \u201920, Curran Associates Inc., Red Hook, NY, USA (2020)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Liu, K., Chen, Z., Liu, Y., Zhang, J.M., Harman, M., Han, Y., Ma, Y., Dong, Y., Li, G., Huang, G.: Llm-powered test case generation for detecting bugs in plausible programs (2025), https:\/\/arxiv.org\/abs\/2404.10304","DOI":"10.18653\/v1\/2025.acl-long.20"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Miltner, A., Padhi, S., Millstein, T., Walker, D.: Data-driven inference of representation invariants. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 1\u201315. PLDI 2020, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3385412.3385967, https:\/\/doi.org\/10.1145\/3385412.3385967","DOI":"10.1145\/3385412.3385967"},{"key":"6_CR20","doi-asserted-by":"publisher","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) (Jul 2024). https:\/\/doi.org\/10.1145\/3643763, https:\/\/doi.org\/10.1145\/3643763","DOI":"10.1145\/3643763"},{"key":"6_CR21","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle. https:\/\/isabelle.in.tum.de (2024), version 2023"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Separation logic. Commun. ACM 62(2), 86\u201395 (Feb 2019). https:\/\/doi.org\/10.1145\/3211968","DOI":"10.1145\/3211968"},{"key":"6_CR23","unstructured":"OpenAI: Openai o1 system card. Technical report, OpenAI (2024), includes safety evaluations and red teaming results for the o1 and o1-mini models"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201905). pp. 247\u2013258. Association for Computing Machinery, New York, NY, USA (2005). https:\/\/doi.org\/10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Perry, N., Srivastava, M., Kumar, D., Boneh, D.: Do users write more insecure code with AI assistants? In: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS). pp. 2785\u20132799. ACM (2023). https:\/\/doi.org\/10.1145\/3576915.3623157","DOI":"10.1145\/3576915.3623157"},{"key":"6_CR26","unstructured":"Poesia, G., Loughridge, C., Amin, N.: dafny-annotator: AI-assisted verification of Dafny programs. CoRR abs\/2411.15143 (2024), https:\/\/arxiv.org\/abs\/2411.15143, arXiv:2411.15143"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002). pp. 55\u201374. IEEE Computer Society, Los Alamitos, CA, USA (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"6_CR28","unstructured":"Sun, C.E., Gao, S., Weng, T.W.: Breaking the barrier: Enhanced utility and robustness in smoothed drl agents. ICML (2024)"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Sun, C., Agashe, V., Chakraborty, S., Taneja, J., Barrett, C.W., Dill, D.L., Qiu, X., Lahiri, S.K.: ClassInvGen: Class invariant synthesis using large language models. CoRR abs\/2502.18917 (2025), https:\/\/arxiv.org\/abs\/2502.18917","DOI":"10.1007\/978-3-031-99991-8_4"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: Closed-loop verifiable code generation. In: AI Verification (SAIV 2024). Lecture Notes in Computer Science, vol. 14846, pp. 134\u2013155. Springer, Cham (2024).https:\/\/doi.org\/10.1007\/978-3-031-65112-0_7","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"6_CR31","unstructured":"The Coq Development Team: The Coq proof assistant. https:\/\/coq.inria.fr (2024), version 8.19.0"},{"key":"6_CR32","unstructured":"Verus Contributors: Verus tutorial and reference (2025), https:\/\/verus-lang.github.io\/verus\/guide\/"},{"key":"6_CR33","unstructured":"Verus Contributors: vstd: Verus standard library api documentation (2025), https:\/\/verus-lang.github.io\/verus\/verusdoc\/vstd\/"},{"key":"6_CR34","unstructured":"Verus Project: Verilib. https:\/\/verilib.org\/, accessed: 2025-02-17"},{"key":"6_CR35","doi-asserted-by":"publisher","unstructured":"Wang, Z., Liu, K., Li, G., Jin, Z.: Hits: High-coverage LLM-based unit test generation via method slicing. In: Proceedings of the 39th IEEE\/ACM International Conference on Automated Software Engineering. p. 1258\u20131268. ASE \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3691620.3695501, https:\/\/doi.org\/10.1145\/3691620.3695501","DOI":"10.1145\/3691620.3695501"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"Wang, Z., Zhou, Z., Song, D., Huang, Y., Chen, S., Ma, L., Zhang, T.: Towards understanding the characteristics of code generation errors made by large language models. In: Proceedings of the 47th IEEE\/ACM International Conference on Software Engineering (ICSE) (2025), to appear","DOI":"10.1109\/ICSE55347.2025.00180"},{"key":"6_CR37","doi-asserted-by":"publisher","unstructured":"Wen, C., Cao, J., Su, J., Xu, Z., Qin, S., He, M., Li, H., Cheung, S.C., Tian, C.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: Computer Aided Verification (CAV 2024). Lecture Notes in Computer Science, vol. 14682, pp. 302\u2013328. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_16","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"6_CR38","unstructured":"Wu, H., Barrett, C., Narodytska, N.: Lemur: Integrating large language models in automated program verification. In: The Twelfth International Conference on Learning Representations"},{"key":"6_CR39","unstructured":"Yang, C., Li, X., Misu, M.R.H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J.R., Lu, S., Yang, F., Zhou, Z., Lu, S.: AutoVerus: Automated proof generation for Rust code. CoRR abs\/2409.13082 (2024), https:\/\/arxiv.org\/abs\/2409.13082"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22749-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:36:36Z","timestamp":1782866196000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","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":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}