{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:07Z","timestamp":1751662867091},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642388552"},{"type":"electronic","value":"9783642388569"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38856-9_14","type":"book-chapter","created":{"date-parts":[[2013,6,15]],"date-time":"2013-06-15T04:05:28Z","timestamp":1371269128000},"page":"238-258","source":"Crossref","is-referenced-by-count":33,"title":["Abstract Semantic Differencing for Numerical Programs"],"prefix":"10.1007","author":[{"given":"Nimrod","family":"Partush","sequence":"first","affiliation":[]},{"given":"Eran","family":"Yahav","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-73368-3_49","volume-title":"Computer Aided Verification","author":"D. Amit","year":"2007","unstructured":"Amit, D., Rinetzky, N., Reps, T., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 477\u2013490. Springer, Heidelberg (2007)"},{"issue":"4","key":"14_CR2","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/s10009-005-0215-8","volume":"8","author":"R. Bagnara","year":"2006","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. Int. J. Softw. Tools Technol. Transf.\u00a08(4), 449\u2013466 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Brumley, D., Poosankam, P., Song, D., Zheng, J.: Automatic patch-based exploit generation is possible: Techniques and implications. In: S&P 2008, pp. 143\u2013157 (2008)","DOI":"10.1109\/SP.2008.17"},{"key":"14_CR4","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209\u2013224 (2008)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-27940-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Chaki","year":"2012","unstructured":"Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 119\u2013135. Springer, Heidelberg (2012)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D.: Hardware verification using ansi-c programs as a reference. In: ASP-DAC, pp. 308\u2013311 (2003)","DOI":"10.1145\/1119772.1119831"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, pp. 84\u201397 (1978)","DOI":"10.1145\/512760.512770"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: DAC, pp. 466\u2013471 (2009)","DOI":"10.1145\/1629911.1630034"},{"issue":"10","key":"14_CR10","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Horwitz, S.: Identifying the semantic and textual differences between two versions of a program. In: PLDI 1990, pp. 234\u2013245 (1990)","DOI":"10.1145\/93548.93574"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Horwitz, S., Prins, J., Reps, T.: Integrating noninterfering versions of programs. ACM Trans. Program. Lang. Syst.\u00a011(3)","DOI":"10.1145\/65979.65980"},{"key":"14_CR13","unstructured":"Hunt, J.W., McIlroy, M.D.: An algorithm for differential file comparison. Tech. rep., Bell Laboratories (1975)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Jackson, D., Ladd, D.A.: Semantic diff: A tool for summarizing the effects of modifications. In: ICSM, pp. 243\u2013252 (1994)","DOI":"10.1109\/ICSM.1994.336770"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Jin, W., Orso, A., Xie, T.: BERT: a tool for behavioral regression testing. In: FSE 2010, pp. 361\u2013362. ACM (2010)","DOI":"10.1109\/ICST.2010.64"},{"key":"14_CR16","unstructured":"Kawaguchi, M., Lahiri, S.\u00a0K., and Rebelo, H. Conditional equivalence. Tech. rep., MSR (2010)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: DAC, pp. 263\u2013268 (1997)","DOI":"10.1145\/266021.266090"},{"key":"14_CR18","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher Order Symbol. Comput.\u00a019, 31\u2013100 (2006)","journal-title":"Higher Order Symbol. Comput."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K., E\u00e9n, N.: Improvements to combinational equivalence checking. In: ICCAD, pp. 836\u2013843 (2006)","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler, pp. 83\u201395","DOI":"10.1145\/358438.349314"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Nethercote, N., Seward, J.: Valgrind: A framework for heavyweight dynamic binary instrumentation. In: PLDI 2007 (2007)","DOI":"10.1145\/1250734.1250746"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Person, S., Dwyer, M.B., Elbaum, S.G., Pasareanu, C.S.: Differential symbolic execution. In: FSE 2008 (2008)","DOI":"10.1145\/1453101.1453131"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, p. 151. Springer, Heidelberg (1998)"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1007\/978-3-642-22110-1_55","volume-title":"Computer Aided Verification","author":"D.A. Ramos","year":"2011","unstructured":"Ramos, D.A., Engler, D.R.: Practical, low-effort equivalence verification of real code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 669\u2013685. Springer, Heidelberg (2011)"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst.\u00a029(5) (August 2007)","DOI":"10.1145\/1275497.1275501"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Song, Y., Zhang, Y., Sun, Y.: Automatic vulnerability locating in binary patches. In: CIS 2009,","DOI":"10.1109\/CIS.2009.273"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T. Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 352\u2013367. Springer, Heidelberg (2005)"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1007\/978-3-642-02658-4_44","volume-title":"Computer Aided Verification","author":"S. Verdoolaege","year":"2009","unstructured":"Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 599\u2013613. Springer, Heidelberg (2009)"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Xin, B., Sumner, W.N., Zhang, X.: Efficient program execution indexing. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 238\u2013248 (2008)","DOI":"10.1145\/1375581.1375611"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Zuck, L., Pnueli, A., Fang, Y., Goldberg, B., Hu, Y.: Translation and run-time validation of optimized code. Electr. Notes Theor. Comput. Sci.\u00a070(4) (2002)","DOI":"10.1016\/S1571-0661(04)80584-X"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38856-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,25]],"date-time":"2022-02-25T08:36:42Z","timestamp":1645778202000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38856-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388552","9783642388569"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38856-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}