{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:29:15Z","timestamp":1767929355014,"version":"3.49.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,3,14]],"date-time":"2008-03-14T00:00:00Z","timestamp":1205452800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2008,7]]},"DOI":"10.1007\/s10817-008-9099-0","type":"journal-article","created":{"date-parts":[[2008,3,13]],"date-time":"2008-03-13T07:29:36Z","timestamp":1205393376000},"page":"1-31","source":"Crossref","is-referenced-by-count":121,"title":["Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations"],"prefix":"10.1007","volume":"41","author":[{"given":"Xavier","family":"Leroy","sequence":"first","affiliation":[]},{"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,3,14]]},"reference":[{"key":"9099_CR1","first-page":"5","volume-title":"Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007, Lecture Notes in Computer Science, vol. 4732","author":"A.W. Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007, Lecture Notes in Computer Science, vol. 4732, pp. 5\u201321. Springer, New York (2007)"},{"key":"9099_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, New York (2004)"},{"key":"9099_CR3","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Int. Symp. on Formal Methods, Lecture Notes in Computer Science, vol. 4085","author":"S. Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: FM 2006: Int. Symp. on Formal Methods, Lecture Notes in Computer Science, vol. 4085, pp. 460\u2013475. Springer, New York (2006)"},{"key":"9099_CR4","first-page":"102","volume-title":"MPC \u201900: Proc. Int. Conf. on Mathematics of Program Construction, Lecture Notes in Computer Science, vol. 1837","author":"R. Bornat","year":"2000","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: MPC \u201900: Proc. Int. Conf. on Mathematics of Program Construction, Lecture Notes in Computer Science, vol. 1837, pp. 102\u2013126. Springer, New York (2000)"},{"key":"9099_CR5","first-page":"23","volume":"7","author":"R. Burstall","year":"1972","unstructured":"Burstall, R.: Some techniques for proving correctness of programs which alter data structures. Mach. Intell. 7, 23\u201350 (1972)","journal-title":"Mach. Intell."},{"key":"9099_CR6","unstructured":"Chrz\u0105szcz, J.: Modules in type theory with generative definitions. Ph.D. thesis, Warsaw University and University of Paris-Sud (2004)"},{"key":"9099_CR7","unstructured":"Conchon, S., Contejean, E., Kanig, J.: The Ergo automatic theorem prover. Software and documentation available at http:\/\/ergo.lri.fr\/ (2005\u20132008)"},{"key":"9099_CR8","unstructured":"Coq development team: The Coq proof assistant. Software and documentation available at http:\/\/coq.inria.fr\/ (1989\u20132008)"},{"key":"9099_CR9","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N., et\u00a0al.: Z3: an efficient SMT solver. Software and documentation available at http:\/\/research.microsoft.com\/projects\/z3 (2006\u20132008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"9099_CR10","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"9099_CR11","first-page":"15","volume-title":"6th Int. Conf. on Formal Engineering Methods, ICFEM 2004, Lecture Notes in Computer Science, vol. 3308","author":"J.C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: Multi-prover verification of C programs. In: 6th Int. Conf. on Formal Engineering Methods, ICFEM 2004, Lecture Notes in Computer Science, vol. 3308, pp. 15\u201329. Springer, New York (2004)"},{"key":"9099_CR12","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C., Moy, Y., Hubert, T.: The Why software verification platform. Software and documentation available at Software and documentation available at http:\/\/why.lri.fr\/ (2004\u20132008)"},{"key":"9099_CR13","unstructured":"ISO: International Standard ISO\/IEC 9899:1999, Programming languages \u2013 C. ISO, Geneva (1999)"},{"key":"9099_CR14","first-page":"131","volume-title":"Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Lecture Notes in Computer Science, vol. 3924","author":"L. Jia","year":"2006","unstructured":"Jia, L., Walker, D.: ILC: a foundation for automated reasoning about pointer programs. In: Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Lecture Notes in Computer Science, vol. 3924, pp. 131\u2013145. Springer, New York (2006)"},{"key":"9099_CR15","first-page":"42","volume-title":"33rd Symposium Principles of Programming Languages","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42\u201354. ACM, New York (2006)"},{"key":"9099_CR16","first-page":"378","volume-title":"32nd Symposium Principles of Programming Languages","author":"J. Manson","year":"2005","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: 32nd Symposium Principles of Programming Languages, pp. 378\u2013391. ACM, New York (2005)"},{"key":"9099_CR17","first-page":"400","volume-title":"Formal Methods and Software Engineering, 8th Int. Conf. ICFEM 2006, Lecture Notes in Computer Science, vol. 4260","author":"N. Marti","year":"2006","unstructured":"Marti, N., Affeldt, R., Yonezawa, A.: Formal verification of the heap manager of an operating system using separation logic. In: Formal Methods and Software Engineering, 8th Int. Conf. ICFEM 2006, Lecture Notes in Computer Science, vol. 4260, pp. 400\u2013419. Springer, New York (2006)"},{"key":"9099_CR18","first-page":"468","volume-title":"Programming Language Design and Implementation 2007","author":"A. McCreight","year":"2007","unstructured":"McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: Programming Language Design and Implementation 2007, pp. 468\u2013479. ACM, New York (2007)"},{"issue":"1\u20132","key":"9099_CR19","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1016\/j.ic.2004.10.007","volume":"199","author":"F. Mehta","year":"2005","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Inf. Comput. 199(1\u20132), 200\u2013227 (2005)","journal-title":"Inf. Comput."},{"key":"9099_CR20","volume-title":"35th Symposium Principles of Programming Languages","author":"M. Nita","year":"2008","unstructured":"Nita, M., Grossman, D., Chambers, C.: A theory of platform-dependent low-level software. In: 35th Symposium Principles of Programming Languages. ACM, New York (2008)"},{"key":"9099_CR21","unstructured":"Norrish, M.: C formalized in HOL. Technical report UCAM-CL-TR-453. Ph.D. thesis, University of Cambridge (1998)"},{"key":"9099_CR22","first-page":"1","volume-title":"Computer Science Logic, 15th Int. Workshop, CSL 2001, Lecture Notes in Computer Science, vol. 2142","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Computer Science Logic, 15th Int. Workshop, CSL 2001, Lecture Notes in Computer Science, vol. 2142, pp. 1\u201319. Springer, New York (2001)"},{"key":"9099_CR23","first-page":"303","volume-title":"Millenial Perspectives in Computer Science","author":"J.C. Reynolds","year":"2000","unstructured":"Reynolds, J.C.: Intuitionistic reasoning about shared data structures. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millenial Perspectives in Computer Science, pp. 303\u2013321. Palgrave, Hampshire (2000)"},{"key":"9099_CR24","first-page":"55","volume-title":"17th Symposium on Logic in Computer Science (LICS 2002)","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th Symposium on Logic in Computer Science (LICS 2002), pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)"},{"key":"9099_CR25","first-page":"150","volume-title":"ISCA \u201999: Proc. Int. Symp. on Computer Architecture","author":"X. Shen","year":"1999","unstructured":"Shen, X., Arvind, R.L.: Commit-reconcile & fences (CRF): a new memory model for architects and compiler writers. In: ISCA \u201999: Proc. Int. Symp. on Computer Architecture, pp. 150\u2013161. IEEE Computer Society, Los Alamitos (1999)"},{"issue":"1\u20132","key":"9099_CR26","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1023\/A:1010022312623","volume":"13","author":"R.D. Tennent","year":"2000","unstructured":"Tennent, R.D., Ghica, D.R.: Abstract models of storage. Higher-Order and Symbolic Computation 13(1\u20132), 119\u2013129 (2000)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"9099_CR27","first-page":"97","volume-title":"34th Symposium Principles of Programming Languages","author":"H. Tuch","year":"2007","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: 34th Symposium Principles of Programming Languages, pp. 97\u2013108. ACM, New York (2007)"},{"issue":"5\u20136","key":"9099_CR28","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1002\/cpe.837","volume":"17","author":"Y. Yang","year":"2005","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: UMM: an operational memory model specification framework with integrated model checking capability. Concurr. Comput.: Practice and Experience 17(5\u20136), 465\u2013487 (2005)","journal-title":"Concurr. Comput.: Practice and Experience"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-008-9099-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-008-9099-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-008-9099-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:48Z","timestamp":1559265708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-008-9099-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3,14]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["9099"],"URL":"https:\/\/doi.org\/10.1007\/s10817-008-9099-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,3,14]]}}}