{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T01:03:33Z","timestamp":1784595813475,"version":"3.55.0"},"reference-count":61,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2026,10]]},"DOI":"10.1016\/j.scico.2026.103535","type":"journal-article","created":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T15:11:12Z","timestamp":1783177872000},"page":"103535","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["From C to verifiable Rust: Towards practical migration of code and specifications"],"prefix":"10.1016","volume":"254","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0907-8985","authenticated-orcid":false,"given":"Shengjie","family":"Xia","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3355-993X","authenticated-orcid":false,"given":"Yijie","family":"Ou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chenghao","family":"Su","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5678-9061","authenticated-orcid":false,"given":"Yimeng","family":"Guo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yanhui","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2352-2226","authenticated-orcid":false,"given":"Lin","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"issue":"10","key":"10.1016\/j.scico.2026.103535_bib0001","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"key":"10.1016\/j.scico.2026.103535_bib0002","series-title":"International Conference on Logic for Programming Artificial Intelligence and Reasoning","first-page":"348","article-title":"Dafny: an automatic program verifier for functional correctness","author":"Leino","year":"2010"},{"issue":"8","key":"10.1016\/j.scico.2026.103535_bib0003","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1145\/3470569","article-title":"The dogged pursuit of bug-free C programs: the Frama-C software analysis platform","volume":"64","author":"Baudin","year":"2021","journal-title":"Commun. ACM"},{"issue":"OOPSLA1","key":"10.1016\/j.scico.2026.103535_bib0004","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1145\/3586037","article-title":"Verus: verifying Rust programs using linear ghost types","volume":"7","author":"Lattuada","year":"2023","journal-title":"Proc. ACM Programm. Lang."},{"key":"10.1016\/j.scico.2026.103535_bib0005","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","article-title":"Satisfiability modulo theories","author":"Barrett","year":"2018","journal-title":"Handbook Model Check."},{"key":"10.1016\/j.scico.2026.103535_bib0006","series-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"337","article-title":"Z3: an efficient SMT solver","author":"De Moura","year":"2008"},{"key":"10.1016\/j.scico.2026.103535_bib0007","series-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"415","article-title":"cvc5: a versatile and industrial-strength SMT solver","author":"Barbosa","year":"2022"},{"key":"10.1016\/j.scico.2026.103535_bib0008","series-title":"SMT Workshop: International Workshop on Satisfiability Modulo Theories","article-title":"Alt-Ergo 2.2","author":"Conchon","year":"2018"},{"key":"10.1016\/j.scico.2026.103535_bib0009","series-title":"NASA Formal Methods Symposium","first-page":"41","article-title":"VeriFast: a powerful, sound, predictable, fast verifier for C and Java","author":"Jacobs","year":"2011"},{"issue":"POPL","key":"10.1016\/j.scico.2026.103535_bib0010","doi-asserted-by":"crossref","first-page":"2069","DOI":"10.1145\/3632911","article-title":"Vst-a: a foundationally sound annotation verifier","volume":"8","author":"Zhou","year":"2024","journal-title":"Proc. ACM Programm. Lang."},{"key":"10.1016\/j.scico.2026.103535_bib0011","series-title":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","first-page":"158","article-title":"RefinedC: automating the foundational verification of C code with refined ownership types","author":"Sammler","year":"2021"},{"issue":"POPL","key":"10.1016\/j.scico.2026.103535_bib0012","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3571194","article-title":"CN: verifying systems C code with separation-logic refinement types","volume":"7","author":"Pulte","year":"2023","journal-title":"Proc. ACM Programm. Lang."},{"key":"10.1016\/j.scico.2026.103535_bib0013","unstructured":"P. Baudin, J.-C. Filli\u00e2tre, C. March\u00e9, B. Monate, Y. Moy, V. Prevosto, Acsl: ANSI\/ISO C specification, (2021)."},{"key":"10.1016\/j.scico.2026.103535_bib0014","doi-asserted-by":"crossref","first-page":"21558","DOI":"10.52202\/075280-0943","article-title":"Is your code generated by chatgpt really correct? Rigorous evaluation of large language models for code generation","volume":"36","author":"Liu","year":"2023","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.scico.2026.103535_bib0015","first-page":"20601","article-title":"Unsupervised translation of programming languages","volume":"33","author":"Roziere","year":"2020","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.scico.2026.103535_bib0016","unstructured":"B. Roziere, J.M. Zhang, F. Charton, M. Harman, G. Synnaeve, G. Lample, Leveraging automated unit tests for unsupervised code translation, (2021)."},{"key":"10.1016\/j.scico.2026.103535_bib0017","series-title":"International Conference on Parallel and Distributed Computing: Applications and Technologies","first-page":"373","article-title":"Equivalence Checking of Code Transformation by Numerical and Symbolic Approaches","author":"Sugawara","year":"2022"},{"key":"10.1016\/j.scico.2026.103535_bib0018","unstructured":"L. Chen, S. Zhang, F. Xu, Z. Xing, L. Wan, X. Zhang, Z. Feng, A test-free semantic mistakes localization framework in neural code translation, (2024)."},{"issue":"1","key":"10.1016\/j.scico.2026.103535_bib0019","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/s10664-023-10385-w","article-title":"Mutation analysis for evaluating code translation","volume":"29","author":"Guizzo","year":"2024","journal-title":"Empirical Softw. Eng."},{"key":"10.1016\/j.scico.2026.103535_bib0020","unstructured":"P. Baudin, F. Bobot, L. Correnson, Z. Dargaye, A. Blanchard, WP plug-in manual, (2025), https:\/\/frama-c.com\/download\/frama-c-wp-manual.pdf."},{"key":"10.1016\/j.scico.2026.103535_bib0021","series-title":"European Symposium on Programming","first-page":"125","article-title":"Why3\u2014where programs meet provers","author":"Filli\u00e2tre","year":"2013"},{"key":"10.1016\/j.scico.2026.103535_bib0022","series-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5\u20139, 2018, Proceedings, Part II 8","first-page":"216","article-title":"Deductive verification of unmodified linux kernel library functions","author":"Efremov","year":"2018"},{"key":"10.1016\/j.scico.2026.103535_bib0023","doi-asserted-by":"crossref","unstructured":"F. Dordowsky, An experimental study using ACSL and Frama-C to formulate and verify low-level requirements from a DO-178C compliant avionics project, (2015).","DOI":"10.4204\/EPTCS.187.3"},{"key":"10.1016\/j.scico.2026.103535_bib0024","series-title":"2024\u202fIEEE 32nd International Requirements Engineering Conference (RE)","first-page":"287","article-title":"Post-hoc formal verification of automotive software with informal requirements: an experience report","author":"Ung","year":"2024"},{"key":"10.1016\/j.scico.2026.103535_bib0025","series-title":"International Symposium on Formal Methods","first-page":"427","article-title":"Formal verification of a JavaCard virtual machine with Frama-C","author":"Djoudi","year":"2021"},{"key":"10.1016\/j.scico.2026.103535_bib0026","series-title":"International Conference on Formal Engineering Methods","first-page":"90","article-title":"Creusot: a foundry for the deductive verification of Rust programs","author":"Denis","year":"2022"},{"key":"10.1016\/j.scico.2026.103535_bib0027","series-title":"NASA Formal Methods Symposium","first-page":"88","article-title":"The prusti project: formal verification for Rust","author":"Astrauskas","year":"2022"},{"key":"10.1016\/j.scico.2026.103535_bib0028","series-title":"Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles","first-page":"438","article-title":"Verus: a practical foundation for systems verification","author":"Lattuada","year":"2024"},{"key":"10.1016\/j.scico.2026.103535_bib0029","series-title":"18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","first-page":"649","article-title":"Anvil: verifying liveness of cluster management controllers","author":"Sun","year":"2024"},{"key":"10.1016\/j.scico.2026.103535_bib0030","series-title":"18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","first-page":"599","article-title":"VeriSMo: a verified security module for confidential VMs","author":"Zhou","year":"2024"},{"key":"10.1016\/j.scico.2026.103535_bib0031","unstructured":"I. Immunant, C2Rust transpiler, 2025, Accessed: 2025-05-30, (https:\/\/github.com\/immunant\/c2rust)."},{"issue":"OOPSLA","key":"10.1016\/j.scico.2026.103535_bib0032","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3485498","article-title":"Translating C to safer Rust","volume":"5","author":"Emre","year":"2021","journal-title":"Proc. ACM Programm. Lang."},{"issue":"OOPSLA1","key":"10.1016\/j.scico.2026.103535_bib0033","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1145\/3586046","article-title":"Aliasing limits on translating C to safe Rust","volume":"7","author":"Emre","year":"2023","journal-title":"Proc. ACM Programm. Lang."},{"key":"10.1016\/j.scico.2026.103535_bib0034","series-title":"Proceedings of the ACM\/IEEE 44th International Conference on Software Engineering: Companion Proceedings","first-page":"354","article-title":"In Rust we trust: a transpiler from unsafe C to safer Rust","author":"Ling","year":"2022"},{"key":"10.1016\/j.scico.2026.103535_bib0035","series-title":"2023 \u202fIEEE\/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)","first-page":"273","article-title":"Improving automatic c-to-Rust translation with static analysis","author":"Hong","year":"2023"},{"issue":"PLDI","key":"10.1016\/j.scico.2026.103535_bib0036","doi-asserted-by":"crossref","first-page":"716","DOI":"10.1145\/3656406","article-title":"Don\u2019t write, but return: replacing output parameters with algebraic data types in C-to-Rust translation","volume":"8","author":"Hong","year":"2024","journal-title":"Proc. ACM Programm. Lang."},{"key":"10.1016\/j.scico.2026.103535_bib0037","series-title":"Proceedings of the 39th IEEE\/ACM International Conference on Automated Software Engineering","first-page":"40","article-title":"To tag, or not to tag: translating C\u2019s Unions to Rust\u2019s tagged unions","author":"Hong","year":"2024"},{"key":"10.1016\/j.scico.2026.103535_bib0038","series-title":"International Conference on Computer Aided Verification","first-page":"459","article-title":"Ownership guided C to Rust translation","author":"Zhang","year":"2023"},{"key":"10.1016\/j.scico.2026.103535_bib0039","series-title":"2025\u202fIEEE\/ACM 47th International Conference on Software Engineering (ICSE)","article-title":"GenC2Rust: towards generating generic Rust code from C","author":"Wu","year":"2025"},{"key":"10.1016\/j.scico.2026.103535_bib0040","unstructured":"M. Shiraishi, T. Shinagawa, Context-aware code segmentation for C-to-Rust translation using large language models, (2024)."},{"key":"10.1016\/j.scico.2026.103535_bib0041","unstructured":"A.Z.H. Yang, Y. Takashima, B. Paulsen, J. Dodds, D. Kroening, Vert: verified equivalent Rust transpilation with few-shot learning, arXiv e-prints (2024) arXiv\u20132404."},{"key":"10.1016\/j.scico.2026.103535_bib0042","unstructured":"H.F. Eniser, H. Zhang, C. David, M. Wang, M. Christakis, B. Paulsen, J. Dodds, D. Kroening, Towards translating real-world code with LLMs: a study of translating to Rust, (2024)."},{"key":"10.1016\/j.scico.2026.103535_bib0043","doi-asserted-by":"crossref","unstructured":"V. Nitin, R. Krishna, L.L.d. Valle, B. Ray, C2SaferRust: transforming C projects into safer Rust with NeuroSymbolic techniques, (2025).","DOI":"10.1109\/TSE.2025.3641486"},{"key":"10.1016\/j.scico.2026.103535_bib0044","series-title":"2025\u202fIEEE 49th Annual Computers, Software, and Applications Conference (COMPSAC)","first-page":"1254","article-title":"C2rusttv: an llm-based framework for C to Rust translation and validation","author":"Zhou","year":"2025"},{"key":"10.1016\/j.scico.2026.103535_bib0045","series-title":"Proceedings of the 14th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis","first-page":"8","article-title":"Optimizing type migration for LLM-based C-to-Rust translation: a data flow graph approach","author":"Xu","year":"2025"},{"key":"10.1016\/j.scico.2026.103535_bib0046","series-title":"International Conference on Engineering of Complex Computer Systems","first-page":"283","article-title":"Rustmap: towards project-scale C-to-Rust migration via program analysis and llm","author":"Cai","year":"2025"},{"issue":"1","key":"10.1016\/j.scico.2026.103535_bib0047","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10664-024-10573-2","article-title":"Type-migrating C-to-Rust translation using a large language model","volume":"30","author":"Hong","year":"2025","journal-title":"Empirical Softw. Eng."},{"issue":"1","key":"10.1016\/j.scico.2026.103535_bib0048","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/s10515-025-00570-0","article-title":"A systematic exploration of C-to-Rust code translation based on large language models: prompt strategies and automated repair","volume":"33","author":"Zhang","year":"2026","journal-title":"Automated Softw. Eng."},{"key":"10.1016\/j.scico.2026.103535_bib0049","unstructured":"M. Brunsfeld, Tree-sitter: a parser generator tool and an incremental parsing library, 2018, Accessed: 2025-05-30, (https:\/\/github.com\/tree-sitter\/tree-sitter)."},{"issue":"7","key":"10.1016\/j.scico.2026.103535_bib0050","doi-asserted-by":"crossref","first-page":"789","DOI":"10.1002\/spe.4380250705","article-title":"ANTLR: a predicated-LL (k) parser generator","volume":"25","author":"Parr","year":"1995","journal-title":"Softw. Pract. Exp."},{"key":"10.1016\/j.scico.2026.103535_bib0051","series-title":"Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution","first-page":"8","article-title":"The E-ACSL perspective on runtime assertion checking","author":"Signoles","year":"2021"},{"key":"10.1016\/j.scico.2026.103535_bib0052","unstructured":"A. Blanchard, J. Gerlach, B. Desloges, A. Lyrakis, Charles, D. Rocha, R. Bachmann, Tutorial WP, 2025, Accessed: 2025-05-30, (https:\/\/github.com\/AllanBlanchard\/tutoriel_wp)."},{"key":"10.1016\/j.scico.2026.103535_bib0053","unstructured":"M. Patnaik, N. Karthikeyan, Frama-C problems, 2020, Accessed: 2025-05-30, (https:\/\/github.com\/manavpatnaik\/frama-c-problems)."},{"key":"10.1016\/j.scico.2026.103535_bib0054","series-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages","first-page":"859","article-title":"LMS-Verify: abstraction without regret for verified systems programming","author":"Amin","year":"2017"},{"key":"10.1016\/j.scico.2026.103535_bib0055","series-title":"International Conference on Computer Aided Verification","first-page":"302","article-title":"Enchanting program specification synthesis by large language models using static analysis and program verification","author":"Wen","year":"2024"},{"issue":"8081","key":"10.1016\/j.scico.2026.103535_bib0056","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1038\/s41586-025-09422-z","article-title":"Deepseek-r1 incentivizes reasoning in llms through reinforcement learning","volume":"645","author":"Guo","year":"2025","journal-title":"Nature"},{"key":"10.1016\/j.scico.2026.103535_bib0057","unstructured":"A. Yang, A. Li, B. Yang, B. Zhang, B. Hui, B. Zheng, B. Yu, C. Gao, C. Huang, C. Lv, et al., Qwen3 technical report, (2025)."},{"key":"10.1016\/j.scico.2026.103535_bib0058","unstructured":"B. Hui, J. Yang, Z. Cui, J. Yang, D. Liu, L. Zhang, T. Liu, J. Zhang, B. Yu, K. Lu, et al., Qwen2. 5-coder technical report, (2024)."},{"key":"10.1016\/j.scico.2026.103535_bib0059","unstructured":"M. Llama, Llama-3.3-70B-Instruct, 2024, Accessed: 2025-07-29, (https:\/\/huggingface.co\/meta-llama\/Llama-3.3-70B-Instruct)."},{"key":"10.1016\/j.scico.2026.103535_bib0060","unstructured":"A. Grattafiori, A. Dubey, A. Jauhri, A. Pandey, A. Kadian, A. Al-Dahle, A. Letman, A. Mathur, A. Schelten, A. Vaughan, A. Yang, A. Fan, A. Goyal, A. Hartshorn, A. Yang, A. Mitra, A. Sravankumar, A. Korenev, A. Hinsvark, A. Rao, A. Zhang, A. Rodriguez, A. Gregerson, A. Spataru, B. Roziere, B. Biron, B. Tang, B. Chern, C. Caucheteux, C. Nayak, C. Bi, C. Marra, C. McConnell, C. Keller, C. Touret, C. Wu, C. Wong, C.C. Ferrer, C. Nikolaidis, D. Allonsius, D. Song, D. Pintz, D. Livshits, D. Wyatt, D. Esiobu, D. Choudhary, D. Mahajan, D. Garcia-Olano, D. Perino, D. Hupkes, E. Lakomkin, E. AlBadawy, E. Lobanova, E. Dinan, E.M. Smith, F. Radenovic, F. Guzm\u00e1n, F. Zhang, G. Synnaeve, G. Lee, G.L. Anderson, G. Thattai, G. Nail, G. Mialon, G. Pang, G. Cucurell, H. Nguyen, H. Korevaar, H. Xu, H. Touvron, I. Zarov, I.A. Ibarra, I. Kloumann, I. Misra, I. Evtimov, J. Zhang, J. Copet, J. Lee, J. Geffert, J. Vranes, J. Park, J. Mahadeokar, J. Shah, J. van der Linde, J. Billock, J. Hong, J. Lee, J. Fu, J. Chi, J. Huang, J. Liu, J. Wang, J. Yu, J. Bitton, J. Spisak, J. Park, J. Rocca, J. Johnstun, J. Saxe, J. Jia, The llama 3 herd of models, arXiv e-prints (2024) arXiv\u20132407."},{"key":"10.1016\/j.scico.2026.103535_bib0061","unstructured":"J. Stone, A. Crichton, \u0141. J. Niemier, M. Blachman, Yoan, V. Steinberg, S. Cappleman-Lynes, num-bigint: big integer types for Rust, 2026, Accessed: 2026-01-28, (https:\/\/crates.io\/crates\/num-bigint)."}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642326001012?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642326001012?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T00:41:26Z","timestamp":1784594486000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642326001012"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,10]]},"references-count":61,"alternative-id":["S0167642326001012"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2026.103535","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2026,10]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"From C to verifiable Rust: Towards practical migration of code and specifications","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2026.103535","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"103535"}}