{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:17:58Z","timestamp":1763468278244,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216898"},{"type":"electronic","value":"9783319216904"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_21","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T02:08:27Z","timestamp":1436926107000},"page":"362-379","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Automatic Rootcausing for Program Equivalence Failures in Binaries"],"prefix":"10.1007","author":[{"given":"Shuvendu K.","family":"Lahiri","sequence":"first","affiliation":[]},{"given":"Rohit","family":"Sinha","sequence":"additional","affiliation":[]},{"given":"Chris","family":"Hawblitzel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: PASTE\u20192005, pp. 82\u201387 (2005)","DOI":"10.1145\/1108768.1108813"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Chandra, S., Torlak, E., Barman, S., Bodik, R.: Angelic debugging. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE\u20192011, pp. 121\u2013130, New York, NY, USA. ACM (2011)","DOI":"10.1145\/1985793.1985811"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Cleve, H., Zeller, A.: Locating causes of program failures. In: Proceedings of the 27th International Conference on Software Engineering, ICSE\u20192005, pp. 342\u2013351, New York, NY, USA. ACM (2005)","DOI":"10.1145\/1062455.1062522"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: POPL, pp. 302\u2013314 (2009)","DOI":"10.1145\/1594834.1480921"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-32759-9_17","volume-title":"FM 2012: Formal Methods","author":"E Ermis","year":"2012","unstructured":"Ermis, E., Sch\u00e4f, M., Wies, T.: Error invariants. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 187\u2013201. Springer, Heidelberg (2012)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: DAC, pp. 466\u2013471 (2009)","DOI":"10.1145\/1629911.1630034"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Lahiri, S.K., Pawar, K., Hashmi, H., Gokbulut, S., Fernando, L., Detlefs, D., Wadsworth, S.: Will you still compile me tomorrow? static cross-version compiler validation. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2013, pp. 191\u2013201, New York, NY, USA. ACM (2013)","DOI":"10.1145\/2491411.2491442"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI\u20192011, pp. 437\u2013446, New York, NY, USA. ACM (2011)","DOI":"10.1145\/1993498.1993550"},{"key":"21_CR9","first-page":"91","volume":"2011","author":"R Konighofer","year":"2011","unstructured":"Konighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. Formal Methods Comput. Aided Des. 2011, 91\u2013100 (2011)","journal-title":"Formal Methods Comput. Aided Des."},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: Programming Language Design and Implementation (PLDI\u20192009), pp. 327\u2013337. ACM (2009)","DOI":"10.1145\/1542476.1542513"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1007\/978-3-642-31424-7_54","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2012","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712\u2013717. Springer, Heidelberg (2012)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2013, pp. 345\u2013355, New York, NY, USA. ACM (2013)","DOI":"10.1145\/2491411.2491452"},{"key":"21_CR13","unstructured":"Lahiri, S.K., Sinha, R., Hawblitzel, C.: Automatic rootcausing for program equivalence failures in binaries. Technical Report MSR-TR-2014-11, Microsoft Research (2014)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u20192000), pp. 83\u201394 (2000)","DOI":"10.1145\/358438.349314"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Nguyen, H.D.T., Qi, D., Roychoudhury, A., Chandra, S.: Semfix: Program repair via semantic analysis. In: Proceedings of the 2013 International Conference on Software Engineering, ICSE\u20192013, pp. 772\u2013781, Piscataway, NJ, USA, IEEE Press (2013)","DOI":"10.1109\/ICSE.2013.6606623"},{"key":"21_CR16","unstructured":"Ramaswamy, S.: Deep dive into the kernel of .NET on Windows Phone 8. In: Build Conference (2012)"},{"key":"21_CR17","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":"DA 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. 6806, pp. 669\u2013685. Springer, Heidelberg (2011)"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Samanta, R., Deshmukh, J.V., Emerson, E.A.: Automatic generation of local repairs for boolean programs. In: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, FMCAD\u20192008, pp. 27:1\u201327:10, Piscataway, NJ, USA. IEEE Press (2008)","DOI":"10.1109\/FMCAD.2008.ECP.31"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Samet, H.: Compiler testing via symbolic interpretation. In: In Proceedings of the ACM 29th Annual Conference, pp. 492\u2013497 (1976)","DOI":"10.1145\/800191.805648"},{"key":"21_CR20","unstructured":"Satisfiability Modulo Theories Library (SMT-LIB). Available \n                      http:\/\/goedel.cs.uiowa.edu\/smtlib\/"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI\u20192013, pp. 15\u201326, New York, NY, USA. ACM (2013)","DOI":"10.1145\/2491956.2462195"},{"issue":"6","key":"21_CR22","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1145\/1273442.1250754","volume":"42","author":"A Solar-Lezama","year":"2007","unstructured":"Solar-Lezama, A., Arnold, G., Tancau, L., Bodik, R., Saraswat, V., Seshia, S.: Sketching stencils. SIGPLAN Not. 42(6), 167\u2013178 (2007)","journal-title":"SIGPLAN Not."},{"key":"21_CR23","unstructured":"SymDiff source code. Available \n                      http:\/\/symdiff.codeplex.com"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Weimer, W.: Patches as better bug reports. In: Generative Programming and Component Engineering, 5th International Conference, GPCE 2006, pp. 181\u2013190. ACM (2006)","DOI":"10.1145\/1173706.1173734"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 99\u2013110 (2010)","DOI":"10.1145\/1806596.1806610"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:07:51Z","timestamp":1563826071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}