{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T16:10:53Z","timestamp":1784391053684,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540003489","type":"print"},{"value":"9783540363842","type":"electronic"}],"license":[{"start":{"date-parts":[[2002,12,16]],"date-time":"2002-12-16T00:00:00Z","timestamp":1039996800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,12,16]],"date-time":"2002-12-16T00:00:00Z","timestamp":1039996800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36384-x_7","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:21:13Z","timestamp":1196328073000},"page":"41-55","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Abstract Interpretation-Based Certification of Assembly Code"],"prefix":"10.1007","author":[{"given":"Xavier","family":"Rival","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"7_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Cache Behavior Prediction by Abstract Interpretation","author":"M. Alt","year":"1996","unstructured":"M. Alt, C. Ferdinand, F. Martin, and R. Wilhelm. Cache Behavior Prediction by Abstract Interpretation. In Static Analysis Symposium, LNCS, 1996."},{"key":"7_CR2","unstructured":"Y. Bertot. A certified compiler for an imperative language. Technical Report RR-3488, INRIA, 1998."},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","volume-title":"The Essence of Computation: Complexity, Analysis, Transformation","author":"B. Blanchet","year":"2002","unstructured":"B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min\u00e9, D. Monniaux, and X. Rival. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, invited chapter. In T. Mogensen, D. Schmidt, and I. Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation, LNCS. Springer-Verlag, 2002. To appear."},{"key":"7_CR4","volume-title":"Program Flow Analysis: Theory and Applications","author":"P. Cousot","year":"1981","unstructured":"P. Cousot. Semantic foundations of program analysis. In S. Muchnick and N. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10. Prentice-Hall, Inc., Englewood Clifis, New Jersey, 1981."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th Symposium on Principles of Programming Languages, 1977.","DOI":"10.1145\/512950.512973"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the 6th Symposium on Principles of Programming Languages. ACM Press, New York, NY, 1979.","DOI":"10.1145\/567752.567778"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program transformation frameworks by abstract interpretation. In Conference Record of the 29th Symposium on Principles of Programming Languages. ACM Press, New York, NY, 2002.","DOI":"10.1145\/503272.503290"},{"key":"7_CR8","unstructured":"C. Ferdinand, F. Martin, and R. Wilhelm. Applying Compiler Techniques to Cache Behavior Prediction. In Workshop on Languages, Compilers and Tools for Real-Time Systems (LCT-RTS), 1997."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"J. Feret. Dependency analysis of mobile systems. In European Symposium on Programming (ESOP\u201902), 2002.","DOI":"10.1007\/3-540-45927-8_22"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"M. Karr. Affine relationships among variables of a program. Acta Informatica, pages 133\u2013151, 1976.","DOI":"10.1007\/BF00268497"},{"key":"7_CR11","unstructured":"A. Min\u00e9. The octagon abstract domain. In AST 2001 in WCRE 2001, IEEE, 2001."},{"key":"7_CR12","unstructured":"G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL\/ML Compiler: Performance and Safety Through Types. In Workshop on Compiler Support for Systems Software, 1996."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"G. C. Necula. Proof-Carrying Code. In Proceedings of the 24th ACM SIGPLANSIGACT Symposium on Principles of Programming Langauges (POPL\u2019 97), 1997.","DOI":"10.1145\/263699.263712"},{"issue":"5","key":"7_CR14","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"G. C. Necula","year":"2000","unstructured":"G. C. Necula. Translation validation for an optimizing compiler. ACM SIGPLAN Notices, 35(5):83\u201394, 2000.","journal-title":"ACM SIGPLAN Notices"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 1955.","DOI":"10.2140\/pjm.1955.5.285"},{"key":"7_CR16","unstructured":"H. Theiling and C. Ferdinand. Combining Abstract Interpretation and ILP for Microarchitecture Modelling and Program Path Analysis. In Proceedings of the 19th IEEE Real-Time Systems Symposium, 1998."},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"H. Theiling, C. Ferdinand, and R. Wilhelm. Fast and Precise WCET Prediction by Seperate Cache and Path Analyses. Real-Time Systems, 2000.","DOI":"10.1023\/A:1008141130870"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"L. Zuck, A. Pnuelli, Y. Fang, and B. Goldberg. VOC: A translation validator for optimizing compilers. In J. Knoop and W. Zimmermann, editors, Electronic Notes in Theoretical Computer Science, volume 65. Elsevier Science Publishers, 2002.","DOI":"10.1016\/S1571-0661(04)80393-1"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36384-X_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T14:20:54Z","timestamp":1778250054000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-36384-X_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12,16]]},"ISBN":["9783540003489","9783540363842"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-36384-x_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002,12,16]]},"assertion":[{"value":"16 December 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}