{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T15:18:08Z","timestamp":1791299888957,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,8,18]],"date-time":"2013-08-18T00:00:00Z","timestamp":1376784000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,8,18]]},"DOI":"10.1145\/2491411.2491429","type":"proceedings-article","created":{"date-parts":[[2013,8,20]],"date-time":"2013-08-20T14:07:21Z","timestamp":1377007641000},"page":"389-399","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["Precision reuse for efficient regression verification"],"prefix":"10.1145","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[{"name":"University of Passau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"L\u00f6we","sequence":"additional","affiliation":[{"name":"University of Passau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Evgeny","family":"Novikov","sequence":"additional","affiliation":[{"name":"ISP RAS, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Stahlbauer","sequence":"additional","affiliation":[{"name":"University of Passau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philipp","family":"Wendler","sequence":"additional","affiliation":[{"name":"University of Passau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2013,8,18]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"99","article-title":"Regression verification using impact summaries. In Proc. SPIN","volume":"7976","author":"Backes J.","year":"2013","unstructured":"J. Backes , S. Person , N. Rungta , and O. Tkachuk . Regression verification using impact summaries. In Proc. SPIN , LNCS 7976 , pp. 99 \u2013 116 . Springer, 2013 . J. Backes, S. Person, N. Rungta, and O. Tkachuk. Regression verification using impact summaries. In Proc. SPIN, LNCS 7976, pp. 99\u2013116. Springer, 2013.","journal-title":"LNCS"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_3_1","volume-title":"Proc. SMT","author":"Barrett C.","year":"2010","unstructured":"C. Barrett , A. Stump , and C. Tinelli . The SMT-LIB Standard: Version 2.0 . In Proc. SMT , 2010 . C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard: Version 2.0. In Proc. SMT, 2010."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"e_1_3_2_1_5_1","first-page":"32","volume-title":"Proc. FMCAD","author":"Beyer D.","unstructured":"D. Beyer , A. Cimatti , A. Griggio , M. E. Keremoglu , and R. Sebastiani . Software model checking via large-block encoding . In Proc. FMCAD , pp. 25\u2013 32 . IEEE, 2009. D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, and R. Sebastiani. Software model checking via large-block encoding. In Proc. FMCAD, pp. 25\u201332. IEEE, 2009."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393664"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_48"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.13"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_26"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032321"},{"key":"e_1_3_2_1_12_1","first-page":"197","volume-title":"Proc. FMCAD","author":"Beyer D.","unstructured":"D. Beyer , M. E. Keremoglu , and P. Wendler . Predicate abstraction with adjustable-block encoding . In Proc. FMCAD , pp. 189\u2013 197 . FMCAD, 2010. D. Beyer, M. E. Keremoglu, and P. Wendler. Predicate abstraction with adjustable-block encoding. In Proc. FMCAD, pp. 189\u2013197. FMCAD, 2010."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34032-1_1"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39176-7_1"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2486829"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_9"},{"key":"e_1_3_2_1_19_1","first-page":"143","volume-title":"Proc. FMCAD","author":"Chockler H.","unstructured":"H. Chockler , A. Ivrii , A. Matsliah , S. Moran , and Z. Nevo . Incremental formal verification of hardware . In Proc. FMCAD , pp. 135\u2013 143 . FMCAD, 2011. H. Chockler, A. Ivrii, A. Matsliah, S. Moran, and Z. Nevo. Incremental formal verification of hardware. In Proc. FMCAD, pp. 135\u2013143. FMCAD, 2011."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_22_1","volume-title":"Regression verification: Proving the equivalence of similar programs. Software Testing, Verification, and Reliability","author":"Godlin B.","year":"2009","unstructured":"B. Godlin and O. Strichman . Regression verification: Proving the equivalence of similar programs. Software Testing, Verification, and Reliability , 2009 . B. Godlin and O. Strichman. Regression verification: Proving the equivalence of similar programs. Software Testing, Verification, and Reliability, 2009."},{"key":"e_1_3_2_1_23_1","first-page":"83","volume-title":"CAV","author":"Graf S.","unstructured":"S. Graf and H. Sa\u00a8\u0131di . Construction of abstract state graphs with Pvs . In CAV , pp. 72\u2013 83 . Springer, 1997. S. Graf and H. Sa\u00a8\u0131di. Construction of abstract state graphs with Pvs. In CAV, pp. 72\u201383. Springer, 1997."},{"key":"e_1_3_2_1_24_1","first-page":"197","volume-title":"Proc. ICSE","author":"Graves T. L.","unstructured":"T. L. Graves , M. J. Harrold , J.-M. Kim , A. A. Porter , and G. Rothermel . An empirical study of regression test selection techniques . In Proc. ICSE , pp. 188\u2013 197 . IEEE, 1998. T. L. Graves, M. J. Harrold, J.-M. Kim, A. A. Porter, and G. Rothermel. An empirical study of regression test selection techniques. In Proc. ICSE, pp. 188\u2013197. IEEE, 1998."},{"key":"e_1_3_2_1_25_1","first-page":"150","volume-title":"Proc. WODES","author":"Hardin R. H.","year":"1996","unstructured":"R. H. Hardin , R. P. Kurshan , K. L. McMillan , J. A. Reeds , and N. J. A. Sloane . E\ufb03cient regression verification . In Proc. WODES , pp. 147\u2013 150 , 1996 . R. H. Hardin, R. P. Kurshan, K. L. McMillan, J. A. Reeds, and N. J. A. Sloane. E\ufb03cient regression verification. In Proc. WODES, pp. 147\u2013150, 1996."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_1_27_1","first-page":"332","article-title":"Extreme model checking. In Proc. Verification: Theory and Practice","volume":"2772","author":"Henzinger T. A.","year":"2003","unstructured":"T. A. Henzinger , R. Jhala , R. Majumdar , and M. A. A. Sanvido . Extreme model checking. In Proc. Verification: Theory and Practice , LNCS 2772 , pp. 332 \u2013 358 . Springer, 2003 . T. A. Henzinger, R. Jhala, R. Majumdar, and M. A. A. Sanvido. Extreme model checking. In Proc. Verification: Theory and Practice, LNCS 2772, pp. 332\u2013358. Springer, 2003.","journal-title":"LNCS"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11486-1_14"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368128"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1134\/S0361768812050039"},{"key":"e_1_3_2_1_32_1","volume-title":"The Art of Software Testing","author":"Myers G. J.","year":"1979","unstructured":"G. J. Myers . The Art of Software Testing . Wiley , 1979 . G. J. Myers. The Art of Software Testing. Wiley, 1979."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993558"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.536955"},{"key":"e_1_3_2_1_35_1","first-page":"121","volume-title":"Proc. FMCAD","author":"Sery O.","unstructured":"O. Sery , G. Fedyukovich , and N. Sharygina . Incremental upgrade checking by means of interpolation-based function summaries . In Proc. FMCAD , pp. 114\u2013 121 . FMCAD, 2012. O. Sery, G. Fedyukovich, and N. Sharygina. Incremental upgrade checking by means of interpolation-based function summaries. In Proc. FMCAD, pp. 114\u2013121. FMCAD, 2012."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/647763.735532"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69149-5_54"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_3_2_1_39_1","first-page":"124","volume-title":"ICSM","author":"Yang G.","unstructured":"G. Yang , M. B. Dwyer , and G. Rothermel . Regression model checking . In ICSM , pp. 115\u2013 124 . IEEE, 2009. G. Yang, M. B. Dwyer, and G. Rothermel. Regression model checking. In ICSM, pp. 115\u2013124. IEEE, 2009."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"}],"event":{"name":"ESEC\/FSE'13: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering","location":"Saint Petersburg Russia","acronym":"ESEC\/FSE'13","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491411.2491429","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2491411.2491429","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:41Z","timestamp":1750231721000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491411.2491429"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8,18]]},"references-count":39,"alternative-id":["10.1145\/2491411.2491429","10.1145\/2491411"],"URL":"https:\/\/doi.org\/10.1145\/2491411.2491429","relation":{},"subject":[],"published":{"date-parts":[[2013,8,18]]},"assertion":[{"value":"2013-08-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}