{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,23]],"date-time":"2026-09-23T07:20:05Z","timestamp":1790148005975,"version":"4.0.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319997247","type":"print"},{"value":"9783319997254","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-99725-4_19","type":"book-chapter","created":{"date-parts":[[2018,8,29]],"date-time":"2018-08-29T17:45:50Z","timestamp":1535564750000},"page":"306-325","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["The Impact of Program Transformations on Static Program Analysis"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zvonimir","family":"Pavlinovic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,8,29]]},"reference":[{"issue":"2","key":"19_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253\u2013284 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR2","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley series in Computer Science\/World Student Series Edition. Addison-Wesley, Reading (1986)"},{"key":"19_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Carter, M., He, S., Whitaker, J., Rakamaric, Z., Emmi, M.: SMACK software verification toolchain. In: Proceedings of the 38th International Conference on Software Engineering - Companion Volume, ICSE 2016, Austin, TX, USA, 14\u201322 May 2016, pp. 589\u2013592 (2016)","DOI":"10.1145\/2889160.2889163"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"81","author":"P Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Constructive versions of Tarski\u2019s fixed point theorems. Pac. J. Math. 81(1), 43\u201357 (1979)","journal-title":"Pac. J. Math."},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-662-46081-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2015","unstructured":"Cousot, P.: Abstracting induction by extrapolation and interpolation. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 19\u201342. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46081-8_2"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program transformation frameworks by abstract interpretation. In: Launchbury, J., Mitchell, J.C. (eds.) Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, 16\u201318 January 2002, pp. 178\u2013190. ACM (2002)","DOI":"10.1145\/503272.503290"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F., Barnett, M.: An abstract interpretation framework for refactoring with application to extract methods with contracts. In: Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, Part of SPLASH 2012, Tucson, AZ, USA, 21\u201325 October 2012, pp. 213\u2013232 (2012)","DOI":"10.1145\/2384616.2384633"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"19_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"EW Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, New York (1990). \nhttps:\/\/doi.org\/10.1007\/978-1-4612-3228-5"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-642-18070-5_2","volume-title":"Formal Verification of Object-Oriented Software","author":"M F\u00e4hndrich","year":"2011","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10\u201330. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-18070-5_2"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-319-41540-6_24","volume-title":"Computer Aided Verification","author":"G Fedyukovich","year":"2016","unstructured":"Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Property directed equivalence via abstract simulation. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part II. LNCS, vol. 9780, pp. 433\u2013453. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41540-6_24"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"771","DOI":"10.1007\/3-540-63165-8_230","volume-title":"Automata, Languages and Programming","author":"R Giacobazzi","year":"1997","unstructured":"Giacobazzi, R., Ranzato, F.: Refining and compressing abstract domains. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 771\u2013781. Springer, Heidelberg (1997). \nhttps:\/\/doi.org\/10.1007\/3-540-63165-8_230"},{"issue":"2","key":"19_CR16","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R Giacobazzi","year":"2000","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361\u2013416 (2000)","journal-title":"J. ACM"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Kang, J., Kim, Y., Song, Y., Lee, J., Park, S., Shin, M.D., Kim, Y., Cho, S., Choi, J., Hur, C.-K., Yi, K.: CRELLVM: verified credible compilation for LLVM. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, 18\u201322 June 2018, pp. 631\u2013645 (2018)","DOI":"10.1145\/3192366.3192377"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE\/ACM International Symposium on Code Generation and Optimization (CGO 2004), San Jose, CA, USA, 20\u201324 March 2004, pp. 75\u201388 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, 11\u201313 January 2006, pp. 42\u201354 (2006)","DOI":"10.1145\/1111037.1111042"},{"issue":"7","key":"19_CR21","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 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-540-78791-4_14","volume-title":"Compiler Construction","author":"F Logozzo","year":"2008","unstructured":"Logozzo, F., F\u00e4hndrich, M.: On the relative completeness of bytecode analysis versus source code analysis. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 197\u2013212. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78791-4_14"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155\u2013172. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-44978-7_10"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-45789-5_11","volume-title":"Static Analysis","author":"A Min\u00e9","year":"2002","unstructured":"Min\u00e9, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 117\u2013132. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45789-5_11"},{"issue":"1","key":"19_CR25","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. High. Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symb. Comput."},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11609773_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Min\u00e9","year":"2005","unstructured":"Min\u00e9, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348\u2013363. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11609773_23"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-36384-X_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KS Namjoshi","year":"2003","unstructured":"Namjoshi, K.S.: Lifting temporal proofs through abstractions. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 174\u2013188. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-36384-X_16"},{"key":"19_CR28","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":"KS Namjoshi","year":"2013","unstructured":"Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 304\u2013323. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38856-9_17"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-45789-5_29","volume-title":"Static Analysis","author":"F Ranzato","year":"2002","unstructured":"Ranzato, F., Tapparo, F.: Making abstract model checking strongly preserving. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 411\u2013427. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45789-5_29"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-24725-8_3","volume-title":"Programming Languages and Systems","author":"F Ranzato","year":"2004","unstructured":"Ranzato, F., Tapparo, F.: Strong preservation as completeness in abstract interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 18\u201332. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24725-8_3"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-540-31980-1_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Ranzato","year":"2005","unstructured":"Ranzato, F., Tapparo, F.: An abstract interpretation-based refinement algorithm for strong preservation. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 140\u2013156. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31980-1_10"},{"issue":"1","key":"19_CR32","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1093\/logcom\/exl035","volume":"17","author":"F Ranzato","year":"2007","unstructured":"Ranzato, F., Tapparo, F.: Generalized strong preservation by abstract interpretation. J. Log. Comput. 17(1), 157\u2013197 (2007)","journal-title":"J. Log. Comput."},{"key":"19_CR33","unstructured":"Rinard, M.: Credible compilation. Technical report (1999). In: Proceedings of CC 2001: International Conference on Compiler Construction"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99725-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,8,29]],"date-time":"2018-08-29T18:04:15Z","timestamp":1535565855000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99725-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319997247","9783319997254"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99725-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}