{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T05:12:45Z","timestamp":1694581965998},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2004,4,6]],"date-time":"2004-04-06T00:00:00Z","timestamp":1081209600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2004,7]]},"DOI":"10.1007\/s10009-003-0125-6","type":"journal-article","created":{"date-parts":[[2004,4,7]],"date-time":"2004-04-07T08:17:12Z","timestamp":1081325832000},"page":"15-37","source":"Crossref","is-referenced-by-count":4,"title":["Certification of compiled assembly code by invariant translation"],"prefix":"10.1007","volume":"6","author":[{"given":"Xavier","family":"Rival","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,4,6]]},"reference":[{"key":"125_CR1","doi-asserted-by":"crossref","unstructured":"Alt M, Ferdinand C, Martin F, Wilhelm R (1996) Cache behavior prediction by abstract interpretation. In: Proceedings of the static analysis symposium (SAS\u201996), September 1996. Lecture notes in computer science, vol 1996. Springer, Berlin Heidelberg New York, pp 51\u201366","DOI":"10.1007\/3-540-61739-6_33"},{"key":"125_CR2","doi-asserted-by":"crossref","unstructured":"Appel AW (2001) Foundational proof-carrying code. In: Proceedings of the 16th symposium on logics in computer science (LICS\u201901), Boston, June 2001, pp 247\u2013256","DOI":"10.1109\/LICS.2001.932501"},{"key":"125_CR3","doi-asserted-by":"crossref","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2002) Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, invited chapter. In: The essence of computation: complexity, analysis, transformation. Essays dedicated to Neil D. Jones. Lecture notes in computer science, vol 2566. Springer, Berlin Heidelberg New York, pp 85\u2013108","DOI":"10.1007\/3-540-36377-7_5"},{"key":"125_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2003) A static analyzer for large safety critical software. In: Proceedings of the ACM SIGPLAN 2003 conference on programming languages, design and implementation (PLDI\u201903), San Diego, October 2003. Lecture notes in computer science, vol 2566. Springer, Berlin Heidelberg New York, pp 85\u2013108","DOI":"10.1145\/780822.781153"},{"key":"125_CR5","unstructured":"Bertot Y (1998) A certified compiler for an imperative language. Technical Report RR-3488, INRIA, 1998"},{"key":"125_CR6","doi-asserted-by":"crossref","unstructured":"Bourdoncle F (1993) Efficient chaotic iteration strategies with widenings. Lecture notes in computer science, vol 735. Springer, Berlin Heidelberg New York, pp 128\u2013141","DOI":"10.1007\/BFb0039704"},{"key":"125_CR7","unstructured":"Cousot P (1981) Semantic foundations of program analysis. In: Program flow analysis: theory and applications, chap 10. Prentice-Hall, Englewood Cliffs, NJ, pp 303\u2013342"},{"key":"125_CR8","doi-asserted-by":"crossref","unstructured":"Cousot P (1997) Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Electron Notes Theor Comput Sci vol 6. Available at: http:\/\/www.elsevier.nl\/locate\/entcs\/volume6.html","DOI":"10.1016\/S1571-0661(05)80168-9"},{"key":"125_CR9","unstructured":"Cousot P (1999) The calculational design of a generic abstract interpreter. In: Calculational system design. NATO ASI Series F. IOS Press, Amsterdam"},{"key":"125_CR10","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) 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 (POPL\u201977), Los Angeles, January 1977, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"125_CR11","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: Conference Record of the 6th symposium on principles of programming languages (POPL\u201979), San Antonio, TX, January 1979. ACM Press, New York, pp 269\u2013282","DOI":"10.1145\/567752.567778"},{"key":"125_CR12","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"Cousot","year":"1992","unstructured":"Cousot P, Cousot R (1992) Abstract interpretation frameworks. J Logic Comput 2(4):511\u2013547","journal-title":"J Logic Comput"},{"key":"125_CR13","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (2002) Systematic design of program transformation frameworks by abstract interpretation. In: Proceedings of the 29th symposium on principles of programming languages (POPL\u201902), Portland, OR, January 2002. ACM Press, New York, pp 178\u2013190","DOI":"10.1145\/565816.503290"},{"key":"125_CR14","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th symposium on principles of programming languages (POPL\u201978), Tucson, AZ, January 1978, pp 84\u201397","DOI":"10.1145\/512760.512770"},{"key":"125_CR15","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1080\/00207168908803778","volume":"30","author":"Granger","year":"1989","unstructured":"Granger P (1989) Static analysis of arithmetical congruences. Int J Comput Math 30:165\u2013190","journal-title":"Int J Comput Math"},{"key":"125_CR16","unstructured":"Handjieva M, Tzolovski S (1998) Refining static analayses by trace-based partitioning using control flow. In: Proceedings of the 5th static analysis symposium (SAS\u201998), Pisa, Italy, September 1998. Lecture notes in computer science, vol 1503. Springer, Berlin Heidelberg New York, pp 200\u2013214"},{"key":"125_CR17","doi-asserted-by":"crossref","unstructured":"Karr M (1976) Affine relationships among variables of a program. Acta Inf 1976, pp 133\u2013151","DOI":"10.1007\/BF00268497"},{"key":"125_CR18","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A (2001) A new numerical abstract domain based on difference-bound matrices. In: Proceedings of the conference on programs as data objects (PADO II), Aahrus, Denmark, May 2001. Lecture notes in computer science, vol 2053. Springer, Berlin Heidelberg New York, pp 155\u2013172","DOI":"10.1007\/3-540-44978-7_10"},{"key":"125_CR19","unstructured":"Morrisett G, Tarditi D, Cheng P, Stone C, Harper R, Lee P (1996) The TIL\/ML compiler: performance and safety through types. In: Proceedings of the workshop on compiler support for systems software, Tucson, AZ, February 1996"},{"key":"125_CR20","unstructured":"Morrisett G, Crary K, Glew N, Grossman D, Samuels R, Smith F, Walker D (1999) TALx86: A realistic typed assembly language. In: Proceedings of the 1999 ACM SIGPLAN workshop on compiler support for system software, Atlanta, GA, May 1999, pp 25\u201335"},{"key":"125_CR21","first-page":"the","volume":"family","author":"Motorola","year":"1997","unstructured":"Motorola (1997) PowerPC microprocessor family: the programming environments for 32-Bit microprocessors, Publication no. G522-0290-01, revised 02\/21\/00","journal-title":"PowerPC microprocessor"},{"key":"125_CR22","doi-asserted-by":"crossref","unstructured":"Necula GC (1997) Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming langauges (POPL\u201997), Paris, January 1997, pp 106\u2013119","DOI":"10.1145\/263699.263712"},{"key":"125_CR23","doi-asserted-by":"crossref","unstructured":"Necula GC (2000) Translation validation for an optimizing compiler. In: Proceedings of the 2000 ACM SIGPLAN conference on programming language design and implementation (PLDI\u201900), Vancouver, BC, Canada, June 2000, pp 83\u201394","DOI":"10.1145\/349299.349314"},{"key":"125_CR24","doi-asserted-by":"crossref","unstructured":"Necula GC, Lee P (1998) The design and implementation of a certifying compiler. In: Proceedings of the ACM SIGPLAN 98 conference on programming languages, design and implementation (PLDI\u201998), Montr\u00e9al, June 1998, pp 333\u2013344","DOI":"10.1145\/277652.277752"},{"key":"125_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli A, Shtrichman O, Siegel M (1998) Translation validation for synchronous languages. In: Prooceedings of the 25th international colloquium on automata, languages and programming (ICALP\u201998), Aahrus, Denmark, July 1998. Lecture notes in computer science, vol 1443. Springer, Berlin Heidelberg New York, pp 235\u2013246","DOI":"10.1007\/BFb0055057"},{"key":"125_CR26","doi-asserted-by":"crossref","unstructured":"Rival X (2003) Abstract interpretation-based certification of assembly code. In: Proceedings of the 4th international conference on verification, model checking and abstract interpretation (VMCAI\u201903), New York, January 2003, pp 41\u201355","DOI":"10.1007\/3-540-36384-X_7"},{"key":"125_CR27","doi-asserted-by":"crossref","unstructured":"Strecker M (2002) Formal verification of a Java compiler in Isabelle. In: Proceedings of the conference on automated deduction (CADE), Copenhagen, Denmark, July 2002. Lecture notes in computer science, vol 2392. Springer, Berlin Heidelberg New York, pp 63\u201377","DOI":"10.1007\/3-540-45620-1_5"},{"key":"125_CR28","doi-asserted-by":"crossref","unstructured":"Tarditi D, Morrisett G, Cheng P, Stone C, Harper R, Lee P (1996) TIL: A type-directed optimizing compiler for ML. In: Proceedings of the ACM SIGPLAN\u201996 conference on programming language design and implementation, May 1996, pp 181\u2013192","DOI":"10.1145\/249069.231414"},{"key":"125_CR29","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"Tarski","year":"1955","unstructured":"Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pacific J Math 5:285\u2013309","journal-title":"Pacific J Math"},{"key":"125_CR30","doi-asserted-by":"crossref","unstructured":"Theiling H, Ferdinand C (1998) Combining abstract interpretation and ILP for microarchitecture modelling and program path analysis. In: Proceedings of the 19th IEEE real-time systems symposium, Madrid, Spain, pp 144\u2013153","DOI":"10.1109\/REAL.1998.739739"},{"key":"125_CR31","doi-asserted-by":"crossref","unstructured":"Theiling H, Ferdinand C, Wilhelm R (2000) Fast and precise WCET prediction by separate cache and path analyses. Real-Time Sys 18:157\u2013179","DOI":"10.1023\/A:1008141130870"},{"key":"125_CR32","doi-asserted-by":"crossref","unstructured":"Zuck L, Pnueli A, Fang Y, Goldberg B (2002) VOC: A translation validator for optimizing compilers. In: Electronic notes in theoretical computer science, vol 65. Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(04)80393-1"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0125-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0125-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0125-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:18Z","timestamp":1559114718000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0125-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4,6]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2004,7]]}},"alternative-id":["125"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0125-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4,6]]}}}