{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:38:47Z","timestamp":1725633527890},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642353079"},{"type":"electronic","value":"9783642353086"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35308-6_5","type":"book-chapter","created":{"date-parts":[[2012,11,8]],"date-time":"2012-11-08T03:20:18Z","timestamp":1352344818000},"page":"11-26","source":"Crossref","is-referenced-by-count":21,"title":["A Formally-Verified Alias Analysis"],"prefix":"10.1007","author":[{"given":"Valentin","family":"Robert","sequence":"first","affiliation":[]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (1994)"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Modern Compiler Implementation in ML. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511811449"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-03153-3_4","volume-title":"Language Engineering and Rigorous Software Development","author":"Y. Bertot","year":"2009","unstructured":"Bertot, Y.: Structural Abstract Interpretation: A Formal Study Using Coq. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) LerNet 2008. LNCS, vol.\u00a05520, pp. 153\u2013194. Springer, Heidelberg (2009)"},{"key":"5_CR4","series-title":"LNCS","first-page":"223","volume-title":"FOSAD 2007\/2008\/2009","author":"F. Besson","year":"2009","unstructured":"Besson, F., Cachera, D., Jensen, T.P., Pichardie, D.: Certified Static Analysis by Abstract Interpretation. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007\/2008\/2009. LNCS, vol.\u00a05705, pp. 223\u2013257. Springer, Heidelberg (2009)"},{"issue":"3","key":"5_CR5","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.08.012","volume":"364","author":"F. Besson","year":"2006","unstructured":"Besson, F., Jensen, T., Pichardie, D.: Proof-carrying code from certified abstract interpretation to fixpoint compression. Theoretical Computer Science\u00a0364(3), 273\u2013291 (2006)","journal-title":"Theoretical Computer Science"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois Connection and Widening\/Narrowing Approaches to Abstract Interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol.\u00a0631, pp. 269\u2013295. Springer, Heidelberg (1992)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-03359-9_16","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Dabrowski","year":"2009","unstructured":"Dabrowski, F., Pichardie, D.: A Certified Data Race Analysis for a Java-like Language. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 212\u2013227. Springer, Heidelberg (2009)"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: haven\u2019t we solved this problem yet? In: Program Analysis For Software Tools and Engineering (PASTE 2001), pp. 54\u201361. ACM (2001)","DOI":"10.1145\/379605.379665"},{"key":"5_CR9","first-page":"194","volume-title":"1st Symposium Principles of Programming Languages","author":"G.A. Kildall","year":"1973","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: 1st Symposium Principles of Programming Languages, pp. 194\u2013206. ACM Press, New York (1973)"},{"key":"5_CR10","first-page":"21","volume-title":"Programming Language Design and Implementation (PLDI 1988)","author":"J.R. Larus","year":"1988","unstructured":"Larus, J.R., Hilfinger, P.N.: Detecting conflicts between structure accesses. In: Programming Language Design and Implementation (PLDI 1988), pp. 21\u201334. ACM Press, New York (1988)"},{"issue":"7","key":"5_CR11","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. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"issue":"4","key":"5_CR12","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"J. Automated Reasoning"},{"key":"5_CR13","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model, version 2. Research report RR-7987, INRIA (June 2012)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Automated Reasoning\u00a041(1) (2008)","DOI":"10.1007\/s10817-008-9099-0"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-32347-8_9","volume-title":"Interactive Theorem Proving","author":"T. Nipkow","year":"2012","unstructured":"Nipkow, T.: Abstract Interpretation of Annotated Commands. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 116\u2013132. Springer, Heidelberg (2012)"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: 23rd Symp. Principles of Programming Languages (POPL 1996), pp. 32\u201341. ACM (1996)","DOI":"10.1145\/237721.237727"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35308-6_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T13:13:50Z","timestamp":1620134030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35308-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642353079","9783642353086"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35308-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}