{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T21:53:47Z","timestamp":1781819627453,"version":"3.54.5"},"reference-count":19,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T00:00:00Z","timestamp":1778025600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Array"],"published-print":{"date-parts":[[2026,7]]},"DOI":"10.1016\/j.array.2026.100879","type":"journal-article","created":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T13:34:39Z","timestamp":1778765679000},"page":"100879","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["An improved method for verifying safe C string programs"],"prefix":"10.1016","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9284-7433","authenticated-orcid":false,"given":"Xuejian","family":"Li","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-7119-7743","authenticated-orcid":false,"given":"Jian","family":"Xing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.array.2026.100879_b1","series-title":"Proof and system-reliability","first-page":"261","article-title":"Proof-carrying code: Design and implementation","author":"Necula","year":"2002"},{"issue":"10","key":"10.1016\/j.array.2026.100879_b2","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"},{"issue":"5","key":"10.1016\/j.array.2026.100879_b3","first-page":"925","article-title":"Research on assertion language with logic variables","volume":"38","author":"Li","year":"2017","journal-title":"J Chin Comput Syst"},{"issue":"5","key":"10.1016\/j.array.2026.100879_b4","first-page":"913","article-title":"Automatic inference of binary tree program loop invariant shape graphs","volume":"38","author":"Li","year":"2017","journal-title":"J Small Microcomput Syst"},{"key":"10.1016\/j.array.2026.100879_b5","series-title":"Design and implementation of safe C language","author":"Li","year":"2016"},{"issue":"5","key":"10.1016\/j.array.2026.100879_b6","first-page":"936","article-title":"Formal verification of stack pointer programs","volume":"38","author":"Feng","year":"2017","journal-title":"J Chin Comput Syst"},{"issue":"1","key":"10.1016\/j.array.2026.100879_b7","first-page":"133","article-title":"Shape checking method in shape system of secure c language verifier","volume":"40","author":"Sun","year":"2019","journal-title":"J Small Microcomput Syst"},{"issue":"2","key":"10.1016\/j.array.2026.100879_b8","first-page":"353","article-title":"An alias detection algorithm for C programs based on stack area memory model","volume":"40","author":"Chang","year":"2019","journal-title":"J Chin Comput Syst"},{"key":"10.1016\/j.array.2026.100879_b9","series-title":"Dafny tutorial","year":"2024"},{"key":"10.1016\/j.array.2026.100879_b10","series-title":"Why3","year":"2024"},{"key":"10.1016\/j.array.2026.100879_b11","series-title":"Z3 prover","year":"2011"},{"key":"10.1016\/j.array.2026.100879_b12","doi-asserted-by":"crossref","unstructured":"Barrett C, et al. CVC4. In: Proc. int. conf. comput. aided verification. Berlin, Germany; 2011, p. 171\u20137.","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"10.1016\/j.array.2026.100879_b13","series-title":"Proc. int. conf. comput. aided verification","first-page":"737","article-title":"Yices 2.2","author":"Dutertre","year":"2014"},{"key":"10.1016\/j.array.2026.100879_b14","series-title":"The coq proof assistant reference manual","author":"The Coq Development Team","year":"2015"},{"key":"10.1016\/j.array.2026.100879_b15","series-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow","year":"2002"},{"key":"10.1016\/j.array.2026.100879_b16","series-title":"ACSL: ANSI\/ISO c specification language","author":"Baudin","year":"2013"},{"key":"10.1016\/j.array.2026.100879_b17","series-title":"Proc. int. symp. formal methods","first-page":"389","article-title":"Z3str4: A multi-armed string solver","author":"Mora","year":"2021"},{"key":"10.1016\/j.array.2026.100879_b18","series-title":"The satisfiability modulo theories library","author":"Barrett","year":"2010"},{"key":"10.1016\/j.array.2026.100879_b19","series-title":"Z3 tutorial","year":"2011"}],"container-title":["Array"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S259000562600202X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S259000562600202X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T21:12:25Z","timestamp":1781817145000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S259000562600202X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":19,"alternative-id":["S259000562600202X"],"URL":"https:\/\/doi.org\/10.1016\/j.array.2026.100879","relation":{},"ISSN":["2590-0056"],"issn-type":[{"value":"2590-0056","type":"print"}],"subject":[],"published":{"date-parts":[[2026,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"An improved method for verifying safe C string programs","name":"articletitle","label":"Article Title"},{"value":"Array","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.array.2026.100879","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Authors. Published by Elsevier Inc.","name":"copyright","label":"Copyright"}],"article-number":"100879"}}