{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T17:09:14Z","timestamp":1725728954203},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642385735"},{"type":"electronic","value":"9783642385742"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38574-2_20","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T07:55:13Z","timestamp":1370332513000},"page":"282-299","source":"Crossref","is-referenced-by-count":35,"title":["Towards Modularly Comparing Programs Using Automated Theorem Provers"],"prefix":"10.1007","author":[{"given":"Chris","family":"Hawblitzel","sequence":"first","affiliation":[]},{"given":"Ming","family":"Kawaguchi","sequence":"additional","affiliation":[]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[]},{"given":"Henrique","family":"Reb\u00ealo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Program Analysis For Software Tools and Engineering (PASTE 2005), pp. 82\u201387 (2005)","DOI":"10.1145\/1108768.1108813"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"6","key":"20_CR3","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/s00236-008-0075-2","volume":"45","author":"B. Godlin","year":"2008","unstructured":"Godlin, B., Strichman, O.: Inference rules for proving the equivalence of recursive procedures. Acta Inf.\u00a045(6), 403\u2013439 (2008)","journal-title":"Acta Inf."},{"key":"20_CR4","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 2009), pp. 327\u2013337. ACM (2009)","DOI":"10.1145\/1542476.1542513"},{"key":"20_CR5","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":"S.K. 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.\u00a07358, pp. 712\u2013717. Springer, Heidelberg (2012)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Lerner, S., Millstein, T.D., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: Programming Language Design and Implementation (PLDI 2003), pp. 220\u2013231 (2003)","DOI":"10.1145\/781154.781156"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Principles of Programming Languages (POPL 2006), pp. 42\u201354 (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: Programming Language Design and Implementation (PLDI 2000), pp. 83\u201394 (2000)","DOI":"10.1145\/358438.349314"},{"key":"20_CR9","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, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"20_CR10","unstructured":"Pnueli, A., Zaks, A.: Validation of interprocedural optimizations. In: Compiler Optimization Meets Compiler Verification (COCV 2008) (2008)"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: Principles of Programming Languages (POPL 2009), pp. 264\u2013276 (2009)","DOI":"10.1145\/1594834.1480915"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Tristan, J., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for llvm. In: Programming Language Design and Implementation (PLDI 2011), pp. 295\u2013305 (2011)","DOI":"10.1145\/1993316.1993533"},{"issue":"3","key":"20_CR13","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/s10703-005-3402-z","volume":"27","author":"L.D. Zuck","year":"2005","unstructured":"Zuck, L.D., Pnueli, A., Goldberg, B., Barrett, C.W., Fang, Y., Hu, Y.: Translation and run-time validation of loop transformations. Formal Methods in System Design\u00a027(3), 335\u2013360 (2005)","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-24"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38574-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T17:56:49Z","timestamp":1557770209000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38574-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385735","9783642385742"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38574-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}