{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T04:06:15Z","timestamp":1725768375374},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_12","type":"book-chapter","created":{"date-parts":[[2014,1,2]],"date-time":"2014-01-02T20:08:09Z","timestamp":1388693289000},"page":"203-221","source":"Crossref","is-referenced-by-count":10,"title":["Weakest Precondition Synthesis for Compiler Optimizations"],"prefix":"10.1007","author":[{"given":"Nuno P.","family":"Lopes","sequence":"first","affiliation":[]},{"given":"Jos\u00e9","family":"Monteiro","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison-Wesley (2006)"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. In: ASPLOS (2006)","DOI":"10.1145\/1168857.1168906"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G. Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 200\u2013214. Springer, Heidelberg (2011)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL (2004)","DOI":"10.1145\/964001.964003"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-28756-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozga","year":"2012","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Deciding conditional termination. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 252\u2013266. Springer, Heidelberg (2012)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/11799573_21","volume-title":"Logic Programming","author":"M. Brain","year":"2006","unstructured":"Brain, M., Crick, T., De Vos, M., Fitch, J.: TOAST: Applying answer set programming to superoptimisation. In: Etalle, S., Truszczy\u0144ski, M. (eds.) ICLP 2006. LNCS, vol.\u00a04079, pp. 270\u2013284. Springer, Heidelberg (2006)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-70545-1_32","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2008","unstructured":"Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 328\u2013340. Springer, Heidelberg (2008)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-35873-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2013","unstructured":"Cousot, P., Cousot, R., F\u00e4hndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 128\u2013148. Springer, Heidelberg (2013)"},{"key":"12_CR10","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":"8","key":"12_CR11","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"issue":"6","key":"12_CR12","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":"12_CR13","doi-asserted-by":"crossref","unstructured":"Goldberg, B., Zuck, L., Barrett, C.: Into the loops: Practical issues in translation validation for optimizing compilers. Electron. Notes Theor. Comp. Sci.\u00a0132 (2005)","DOI":"10.1016\/j.entcs.2005.01.030"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI (2011)","DOI":"10.1145\/1993498.1993506"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-540-93900-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 120\u2013135. Springer, Heidelberg (2009)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Guo, S.-Y., Palsberg, J.: The essence of compiling with traces. In: POPL (2011)","DOI":"10.1145\/1926385.1926450"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-642-38574-2_20","volume-title":"Automated Deduction \u2013 CADE-24","author":"C. Hawblitzel","year":"2013","unstructured":"Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Reb\u00ealo, H.: Towards modularly comparing programs using automated theorem provers. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 282\u2013299. Springer, Heidelberg (2013)"},{"issue":"6","key":"12_CR18","doi-asserted-by":"publisher","first-page":"967","DOI":"10.1145\/1186632.1186633","volume":"28","author":"R. Joshi","year":"2006","unstructured":"Joshi, R., Nelson, G., Zhou, Y.: Denali: A practical algorithm for generating optimal code. ACM Trans. Program. Lang. Syst.\u00a028(6), 967\u2013989 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR19","unstructured":"Junker, U.: QUICKXPLAIN: Preferred explanations and relaxations for over-constrained problems. In: AAAI (2004)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: PLDI (2009)","DOI":"10.1145\/1542476.1542513"},{"issue":"6","key":"12_CR21","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett.\u00a093(6), 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: PLDI (2003)","DOI":"10.1145\/781131.781156"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Lerner, S., Millstein, T., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. In: POPL (2005)","DOI":"10.1145\/1040305.1040335"},{"issue":"7","key":"12_CR24","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-642-39176-7_18","volume-title":"Model Checking Software","author":"N.P. Lopes","year":"2013","unstructured":"Lopes, N.P., Monteiro, J.: Automatic equivalence checking of UF+IA programs. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol.\u00a07976, pp. 282\u2013300. Springer, Heidelberg (2013)"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-39799-8_39","volume-title":"Computer Aided Verification","author":"J. Marques-Silva","year":"2013","unstructured":"Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 592\u2013607. Springer, Heidelberg (2013)"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-78163-9_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y. Moy","year":"2008","unstructured":"Moy, Y.: Sufficient preconditions for modular assertion checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 188\u2013202. Springer, Heidelberg (2008)"},{"key":"12_CR28","unstructured":"Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann (1997)"},{"key":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-38856-9_17","volume-title":"Static Analysis","author":"K.S. Namjoshi","year":"2013","unstructured":"Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 304\u2013323. Springer, Heidelberg (2013)"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI (2000)","DOI":"10.1145\/349299.349314"},{"key":"12_CR31","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":"12_CR32","doi-asserted-by":"crossref","unstructured":"Scherpelz, E.R., Lerner, S., Chambers, C.: Automatic inference of optimizer flow functions from semantic meanings. In: PLDI (2007)","DOI":"10.1145\/1250734.1250750"},{"key":"12_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-642-37036-6_25","volume-title":"Programming Languages and Systems","author":"M.N. Seghir","year":"2013","unstructured":"Seghir, M.N., Kroening, D.: Counterexample-guided precondition inference. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 451\u2013471. Springer, Heidelberg (2013)"},{"key":"12_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-642-22110-1_59","volume-title":"Computer Aided Verification","author":"M. Stepp","year":"2011","unstructured":"Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 737\u2013742. Springer, Heidelberg (2011)"},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: POPL (2009)","DOI":"10.1145\/1594834.1480915"},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Generating compiler optimizations from proofs. In: POPL (2010)","DOI":"10.1145\/1706299.1706345"},{"key":"12_CR37","doi-asserted-by":"crossref","unstructured":"Tatlock, Z., Lerner, S.: Bringing extensibility to verified compilers. In: PLDI (2010)","DOI":"10.1145\/1806596.1806611"},{"key":"12_CR38","doi-asserted-by":"crossref","unstructured":"Tristan, J.-B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: PLDI (2011)","DOI":"10.1145\/1993498.1993533"},{"key":"12_CR39","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: PLDI (2011)","DOI":"10.1145\/1993498.1993532"},{"key":"12_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-68237-0_5","volume-title":"FM 2008: Formal Methods","author":"A. Zaks","year":"2008","unstructured":"Zaks, A., Pnueli, A.: CoVaC: Compiler validation by program analysis of the cross-product. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 35\u201351. Springer, Heidelberg (2008)"},{"key":"12_CR41","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formal verification of SSA-based optimizations for LLVM. In: PLDI (2013)","DOI":"10.1145\/2491956.2462164"},{"key":"12_CR42","doi-asserted-by":"crossref","unstructured":"Zuck, L., Pnueli, A., Goldberg, B., Barrett, C., Fang, Y., Hu, Y.: Translation and run-time validation of loop transformations. Form. Methods Syst. Des.\u00a027 (2005)","DOI":"10.1007\/s10703-005-3402-z"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54013-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T19:44:08Z","timestamp":1558813448000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}