{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T14:33:12Z","timestamp":1754145192052,"version":"3.41.2"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"ISSTA","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["No. U2341212, No. 62032024"],"award-info":[{"award-number":["No. U2341212, No. 62032024"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012166","name":"National key R\\\\&D program of China","doi-asserted-by":"crossref","award":["No. 2022YFB4501903"],"award-info":[{"award-number":["No. 2022YFB4501903"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2025,6,22]]},"abstract":"<jats:p>Programs evolve continuously throughout their life cycles.  \nVerifying each version from scratch is usually impractical, especially for concurrent programs.  \nDesigning efficient incremental verification techniques for concurrent programs is highly desired.  \nWe focus on the abstraction refinement technique for concurrent program verification.  \nWhen a program is modified, those refinement constraints generated in the verifications of previous versions are adapted to the new program to avoid redundant analysis.  \nWe propose a kernel source based refinement constraint adaptation approach for the scheduling constraint based abstraction refinement method, one of the most efficient abstraction refinement methods for concurrent program verification.  \nOur method supports all kinds of program modifications, and generates adapted refinement constraints according to the modifications.  \nEvaluation on the benchmarks from SV-COMP 2024 and Nidhugg benchmarks shows promising results of our method.  \nMost of the refinement constraints generated in the verification of previous versions can be adapted to the modified program in our experiments.  \nCompared with verifying the modified program from scratch, our incremental verification method can achieve two orders of magnitude speedup for those complex programs.<\/jats:p>","DOI":"10.1145\/3728976","type":"journal-article","created":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T10:52:56Z","timestamp":1750589576000},"page":"2251-2272","source":"Crossref","is-referenced-by-count":0,"title":["Incremental Verification of Concurrent Programs through Refinement Constraint Adaptation"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1645-2787","authenticated-orcid":false,"given":"Liangze","family":"Yin","sequence":"first","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-3329-810X","authenticated-orcid":false,"given":"Yiwei","family":"Li","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-6300-238X","authenticated-orcid":false,"given":"Kun","family":"Chen","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8033-7943","authenticated-orcid":false,"given":"Wei","family":"Dong","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0637-8744","authenticated-orcid":false,"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10766-017-0548-4"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39176-7_7"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409757"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491429"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606576"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-018-0322-2"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-015-0237-0"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314596"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_21"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642987"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Fei He Shu Mao and Bow-Yaw Wang. 2016. Learning-Based Assume-Guarantee Regression Verification. In Computer Aided Verification (CAV). 310\u2013328. https:\/\/doi.org\/10.1007\/978-3-319-41528-4_17 10.1007\/978-3-319-41528-4_17","DOI":"10.1007\/978-3-319-41528-4_17"},{"key":"e_1_2_1_13_1","volume-title":"When Regression Verification Meets CEGAR. CoRR, abs\/1806.04829","author":"He Fei","year":"2018","unstructured":"Fei He, Qianshan Yu, and Liming Cai. 2018. When Regression Verification Meets CEGAR. CoRR, abs\/1806.04829 (2018), arxiv:1806.04829"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.3021477"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/FORMALISE52586.2021.00019"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368128"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192390"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527332"},{"key":"e_1_2_1_19_1","unstructured":"Nidhugg. 2025. Nidhugg benchmark.. https:\/\/github.com\/nidhugg\/nidhugg\/tree\/master\/benchmarks\/"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2207.14364"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_8"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_39"},{"key":"e_1_2_1_23_1","unstructured":"SV-COMP. 2017. 2017 software verification competition.. http:\/\/sv-comp.sosy-lab.org\/2017\/"},{"key":"e_1_2_1_24_1","unstructured":"SV-COMP. 2018. 2018 software verification competition.. http:\/\/sv-comp.sosy-lab.org\/2018\/"},{"key":"e_1_2_1_25_1","unstructured":"SV-COMP. 2019. 2019 software verification competition.. http:\/\/sv-comp.sosy-lab.org\/2019\/"},{"key":"e_1_2_1_26_1","unstructured":"SV-COMP. 2024. 2024 software verification competition.. http:\/\/sv-comp.sosy-lab.org\/2024\/"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.45"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579027.3608978"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00145"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_25"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2018.2864122"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428252"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950332"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3728976","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T16:45:34Z","timestamp":1752684334000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3728976"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,22]]},"references-count":34,"journal-issue":{"issue":"ISSTA","published-print":{"date-parts":[[2025,6,22]]}},"alternative-id":["10.1145\/3728976"],"URL":"https:\/\/doi.org\/10.1145\/3728976","relation":{},"ISSN":["2994-970X"],"issn-type":[{"type":"electronic","value":"2994-970X"}],"subject":[],"published":{"date-parts":[[2025,6,22]]}}}