{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T17:17:13Z","timestamp":1764350233299,"version":"3.40.5"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662460801"},{"type":"electronic","value":"9783662460818"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_17","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T09:25:44Z","timestamp":1418289944000},"page":"300-317","source":"Crossref","is-referenced-by-count":8,"title":["From Verification to Optimizations"],"prefix":"10.1007","author":[{"given":"Rigel","family":"Gjomemo","sequence":"first","affiliation":[]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[]},{"given":"Phu H.","family":"Phung","sequence":"additional","affiliation":[]},{"given":"V. N.","family":"Venkatakrishnan","sequence":"additional","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., Hawkins, P.: An overview of the Saturn project. In: 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE), pp. 43\u201348 (2007)","DOI":"10.1145\/1251535.1251543"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/978-3-642-36742-7_52","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., Gurfinkel, A., Li, Y., Chaki, S., Chechik, M.: UFO: Verification with interpolants and abstract interpretation. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 637\u2013640. Springer, Heidelberg (2013)"},{"issue":"1","key":"17_CR3","first-page":"5","volume":"9","author":"R. Bonichon","year":"2011","unstructured":"Bonichon, R., Cuoq, P.: A mergeable interval map. Studia Informatica Universalis\u00a09(1), 5\u201337 (2011)","journal-title":"Studia Informatica Universalis"},{"key":"17_CR4","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Conference on Operating Systems Design and Implementation, OSDI 2008, pp. 209\u2013224. USENIX Association (2008)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P. Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C, A software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 233\u2013247. Springer, Heidelberg (2012)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: 28th Annual ACM Symposium on Applied Computing, SAC, pp. 1230\u20131235 (2013)","DOI":"10.1145\/2480362.2480593"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Dhurjati, D., Adve, V.: Backwards-Compatible Array Bounds Checking for C with Very Low Overhead. Technical report, Shanghai, China (May 2006)","DOI":"10.1145\/1134285.1134309"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Dietz, W., Li, P., Regehr, J., Adve, V.: Understanding integer overflow in C\/C++. In: 34th International Conference on Software Engineering, ICSE 2012, pp. 760\u2013770. IEEE Press (2012)","DOI":"10.1109\/ICSE.2012.6227142"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Grosser, T., Gr\u00f6\u00dflinger, A., Lengauer, C.: Polly \u2013 performing polyhedral optimizations on a low-level intermediate representation. Parallel Processing Letters\u00a022(4) (2012)","DOI":"10.1142\/S0129626412500107"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-SOFT: Software Verification Platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: CGO, pp. 75\u201388 (2004), llvm.org","DOI":"10.1109\/CGO.2004.1281665"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Extended Static Checking: A ten-year perspective. In: Informatics \u2013 10 Years Back. 10 Years Ahead, pp. 157\u2013175 (2001)","DOI":"10.1007\/3-540-44577-3_11"},{"key":"17_CR14","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-38856-9_17"},{"issue":"3","key":"17_CR15","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1145\/1065887.1065892","volume":"27","author":"G.C. Necula","year":"2005","unstructured":"Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: CCured: Type-safe retrofitting of legacy software. ACM Trans. Program. Lang. Syst.\u00a027(3), 477\u2013526 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-48257-1_8","volume-title":"Applied Formal Methods - FM-Trends 98","author":"A. Pnueli","year":"1999","unstructured":"Pnueli, A., Strichman, O., Siegel, M.: Translation validation: From DC+ to c*. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol.\u00a01641, pp. 137\u2013150. Springer, Heidelberg (1999)"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Teitelbaum, T.: Codesurfer. ACM SIGSOFT Software Engineering Notes\u00a025(1) (2000)","DOI":"10.1145\/340855.341076"}],"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-662-46081-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T00:37:08Z","timestamp":1747183028000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}