{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,18]],"date-time":"2024-04-18T15:51:56Z","timestamp":1713455516826},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","funder":[{"DOI":"10.13039\/501100012659","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61672310"],"id":[{"id":"10.13039\/501100012659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007162","name":"Guangdong Science and Technology Department","doi-asserted-by":"publisher","award":["2018B010107004"],"id":[{"id":"10.13039\/501100007162","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100013290","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2018YFB1308601"],"id":[{"id":"10.13039\/501100013290","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"Software products are evolving during their life cycles. Ideally, every revision need be formally verified to ensure software quality. Yet repeated formal verification requires significant computing resources. Verifying each and every revision can be very challenging. It is desirable to ameliorate regression verification for practical purposes. In this paper, we regard predicate analysis as a process of assertion annotation. Assertion annotations can be used as a certificate for the verification results. It is thus a waste of resources to throw them away after each verification. We propose to reuse the previously-yielded assertion annotation in regression verification. A light-weight impact-analysis technique is proposed to analyze the reusability of assertions. A novel assertion strengthening technique is furthermore developed to improve reusability of annotation. With these techniques, we present an incremental predicate analysis technique for regression verification. Correctness of our incremental technique is formally proved. We performed comprehensive experiments on revisions of Linux kernel device drivers. Our technique outperforms the state-of-the-art program verification tool CPAchecker by getting 2.8x speedup in total time and solving additional 393 tasks.<\/jats:p>","DOI":"10.1145\/3428252","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-25","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Incremental predicate analysis for regression verification"],"prefix":"10.1145","volume":"4","author":[{"ORCID":"http:\/\/orcid.org\/0000-0003-4584-6125","authenticated-orcid":false,"given":"Qianshan","family":"Yu","sequence":"first","affiliation":[{"name":"Tsinghua University, China"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-4266-875X","authenticated-orcid":false,"given":"Fei","family":"He","sequence":"additional","affiliation":[{"name":"Tsinghua University, China"}]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taiwan"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227120"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSMR.2000.827331"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062534"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771802"},{"key":"e_1_2_2_5_1","volume-title":"Software Change Impact Analysis","author":"Arnold Robert S.","unstructured":"Robert S. Arnold . 1996. Software Change Impact Analysis . IEEE Computer Society Press , Washington, DC, USA . Robert S. Arnold. 1996. Software Change Impact Analysis. IEEE Computer Society Press, Washington, DC, USA."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_25"},{"key":"e_1_2_2_8_1","volume-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories","volume":"13","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett , Aaron Stump , Cesare Tinelli , 2010 . The SMT-LIB standard: Version 2.0 . In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories ( Edinburgh, England) , Vol. 13 . 14. Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The SMT-LIB standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England), Vol. 13. 14."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1998496.1998532"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491429"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_29"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2004.1357834"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_9"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00058-8"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_30"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_16"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_25"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_24"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_21"},{"key":"e_1_2_2_26_1","volume-title":"Lyle","author":"Gallagher Keith Brian","year":"1991","unstructured":"Keith Brian Gallagher and James R . Lyle . 1991 . Using program slicing in software maintenance. IEEE transactions on software engineering 17, 8 ( 1991 ), 751-761. https:\/\/doi.org\/10.1.1.39.1532 Keith Brian Gallagher and James R. Lyle. 1991. Using program slicing in software maintenance. IEEE transactions on software engineering 17, 8 ( 1991 ), 751-761. https:\/\/doi.org\/10.1.1.39.1532"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_12"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629911.1630034"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_17"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39910-0_16"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_17"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11486-1_14"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0293-8"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491452"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368128"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/7261"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.1998.738510"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/METRIC.1997.637156"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1134\/S0361768812050039"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2002.994702"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940089"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_22"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379661"},{"key":"e_1_2_2_50_1","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"Sery Ondrej","year":"2012","unstructured":"Ondrej Sery , Grigory Fedyukovich , and Natasha Sharygina . 2012. Incremental upgrade checking by means of interpolationbased function summaries . In Formal Methods in Computer-Aided Design (FMCAD) , 2012 (Cambridge, UK ). IEEE Press , New York, NY, USA, 114-121. http:\/\/ieeexplore.ieee.org\/document\/6462563\/ Ondrej Sery, Grigory Fedyukovich, and Natasha Sharygina. 2012. Incremental upgrade checking by means of interpolationbased function summaries. In Formal Methods in Computer-Aided Design (FMCAD), 2012 (Cambridge, UK). IEEE Press, New York, NY, USA, 114-121. http:\/\/ieeexplore.ieee.org\/document\/6462563\/"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.536959"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34281-3_24"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2009.5306334"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629536"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428252","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T21:43:36Z","timestamp":1672609416000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428252"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":55,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428252"],"URL":"https:\/\/doi.org\/10.1145\/3428252","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}
