{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T03:57:02Z","timestamp":1648871822074},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,12,21]],"date-time":"2010-12-21T00:00:00Z","timestamp":1292889600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2011,2]]},"DOI":"10.1007\/s10703-010-0108-7","type":"journal-article","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T13:26:02Z","timestamp":1292851562000},"page":"33-61","source":"Crossref","is-referenced-by-count":6,"title":["Certifying compilers using higher-order theorem provers as certificate checkers"],"prefix":"10.1007","volume":"38","author":[{"given":"Jan Olaf","family":"Blech","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,12,21]]},"reference":[{"key":"108_CR1","volume-title":"Logic in computer science (LICS \u201990)","author":"SF Allen","year":"1990","unstructured":"Allen SF, Constable RL, Howe DJ, Aitken W (1990) The semantics of reflected proofs. In: Logic in computer science (LICS \u201990). IEEE Computer Society Press, Los Alamitos"},{"key":"108_CR2","volume-title":"Logic in computer science (LICS \u201901)","author":"AW Appel","year":"2001","unstructured":"Appel AW (2001) Foundational proof-carrying code. In: Logic in computer science (LICS \u201901). IEEE Computer Society Press, Los Alamitos"},{"key":"108_CR3","series-title":"LNCS","volume-title":"Compiler construction (CC \u201992)","author":"B Buth","year":"1992","unstructured":"Buth B, Buth K-H, Fr\u00e4nzle M, von Karger B, Lakhnech Y, Langmaack H, M\u00fcller-Olm M (1992) Provably correct compiler development and implementation. In: Compiler construction (CC \u201992). LNCS. Springer, Berlin"},{"key":"108_CR4","series-title":"LNCS","volume-title":"Computer aided verification (CAV \u201905)","author":"C Barrett","year":"2005","unstructured":"Barrett C, Fang Y, Goldberg B, Hu Y, Pnueli A, Zuck L (2005) TVOC: a translation validator for optimizing compilers. In: Computer aided verification (CAV \u201905). LNCS. vol 3576. Springer, Berlin"},{"key":"108_CR5","series-title":"ENTCS","volume-title":"Compiler optimization meets compiler verification (COCV \u201908)","author":"JO Blech","year":"2008","unstructured":"Blech JO, Gr\u00e9goire B (2008) Certifying code generation with coq. In: Compiler optimization meets compiler verification (COCV \u201908), April 2008. ENTCS. Elsevier, Amsterdam"},{"key":"108_CR6","volume-title":"Compiler optimization meets compiler verification (COCV \u201909)","author":"JO Blech","year":"2009","unstructured":"Blech JO, Gr\u00e9goire B (2009) Using checker predicates in certifying code generation. In: Compiler optimization meets compiler verification (COCV \u201909), March 2009. Elsevier, Amsterdam"},{"key":"108_CR7","volume-title":"Compiler optimization meets compiler verification (COCV \u201905)","author":"JO Blech","year":"2005","unstructured":"Blech JO, Glesner S, Leitner J, M\u00fclling S (2005) Optimizing code generation from SSA form: a comparison between two formal correctness proofs in Isabelle\/HOL. In: Compiler optimization meets compiler verification (COCV \u201905), April 2005. Elsevier, Amsterdam"},{"key":"108_CR8","unstructured":"Blech JO (2007) On certifying code generation. Technical Report 366\/07, University of Kaiserslautern, November 2007"},{"key":"108_CR9","series-title":"PhD-Thesis","isbn-type":"print","volume-title":"Certifying system translations using higher order theorem provers","author":"JO Blech","year":"2009","unstructured":"Blech JO (2009) Certifying system translations using higher order theorem provers. PhD-Thesis. Logos, Berlin, ISBN\u00a03832522115","ISBN":"http:\/\/id.crossref.org\/isbn\/3832522115"},{"key":"108_CR10","series-title":"LNCS","volume-title":"Theorem proving in higher order logics","author":"S Berghofer","year":"2000","unstructured":"Berghofer S, Nipkow T (2000) Proof terms for simply typed higher order logic. In: Theorem proving in higher order logics. LNCS. Springer, Berlin"},{"key":"108_CR11","volume-title":"Software and compilers for embedded systems (SCOPES \u201909)","author":"JO Blech","year":"2009","unstructured":"Blech JO, P\u00e9rin M (2009) Using checker predicates in certifying code generation. In: Software and compilers for embedded systems (SCOPES \u201909), April 2009"},{"key":"108_CR12","doi-asserted-by":"crossref","unstructured":"Blech JO, P\u00e9rin M (2011) Generating invariant-based certificates for embedded systems. In ACM Trans Embed Comput Syst (TECS) (to appear)","DOI":"10.1145\/2220336.2220346"},{"key":"108_CR13","series-title":"ENTCS","volume-title":"Compiler optimization meets compiler verification (COCV \u201907)","author":"JO Blech","year":"2007","unstructured":"Blech JO, Poetzsch-Heffter A (2007) A certifying code generation phase. In: Compiler optimization meets compiler verification (COCV \u201907), March 2007. ENTCS. Elsevier, Amsterdam"},{"key":"108_CR14","series-title":"LNCS","volume-title":"Runtime verification (RV \u201907)","author":"JO Blech","year":"2007","unstructured":"Blech JO, Schaefer I, Poetzsch-Heffter A (2007) Translation validation of system abstractions. In: Runtime verification (RV \u201907), March 2007. LNCS. vol 4839. Springer, Berlin"},{"key":"108_CR15","series-title":"LNCS","volume-title":"Theoretical aspects of computer software (TACS \u201997)","author":"S Boutin","year":"1997","unstructured":"Boutin S (1997) Using reflection to build efficient and certified decision procedures. In: Theoretical aspects of computer software (TACS \u201997). LNCS. Springer, Berlin"},{"key":"108_CR16","series-title":"LNCS","volume-title":"Formal methods in the development of computing systems","author":"B Chetali","year":"2008","unstructured":"Chetali B, Nguyen QH (2008) Industrial use of formal methods for a high-level security evaluation. In: Formal methods in the development of computing systems. LNCS, vol 5014. Springer, Berlin"},{"key":"108_CR17","doi-asserted-by":"crossref","unstructured":"Dave M (2003) Compiler verification: a bibliography. ACM SIGSOFT Softw Eng Notes","DOI":"10.1145\/966221.966235"},{"key":"108_CR18","unstructured":"Gawkowski MJ, Blech JO, Poetzsch-Heffter A (2006) Certifying compilers based on formal translation contracts. Technical Report 355-06, University of Kaiserslautern, November 2006"},{"key":"108_CR19","series-title":"LNCS","volume-title":"Functional and logic programming, 8th international symposium","author":"B Gr\u00e9goire","year":"2006","unstructured":"Gr\u00e9goire B, Th\u00e9ry L, Werner B (2006) A computational approach to Pocklington certificates in type theory. In: Functional and logic programming, 8th international symposium. LNCS. Springer, Berlin"},{"key":"108_CR20","series-title":"LNCS","volume-title":"Theorem proving in higher order logics (TPHOLs \u201905)","author":"B Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire B, Mahboubi A (2005) Proving equalities in a commutative ring done right in Coq. In: Theorem proving in higher order logics (TPHOLs \u201905). LNCS. Springer, Berlin"},{"key":"108_CR21","series-title":"LNCS","volume-title":"Correct system design","author":"G Goos","year":"1999","unstructured":"Goos G, Zimmermann W (1999) Verification of compilers. In: Steffen B, Olderog ER (eds) Correct system design, November 1999. LNCS, vol 1710. Springer, Berlin"},{"key":"108_CR22","unstructured":"Kaufmann M, Moore J (2010) ACL2 homepage. See URL http:\/\/www.cs.-utexas.edu\/users\/moore\/acl2"},{"issue":"4","key":"108_CR23","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G Klein","year":"2006","unstructured":"Klein G, Nipkow T (2006) A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans Program Lang Syst 28(4):619\u2013695","journal-title":"ACM Trans Program Lang Syst"},{"key":"108_CR24","first-page":"42","volume-title":"Principles of programming languages (POPL \u201906)","author":"X Leroy","year":"2006","unstructured":"Leroy X (2006) Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Principles of programming languages (POPL \u201906). ACM Press, New York, pp 42\u201354"},{"key":"108_CR25","volume-title":"Principles of programming languages (POPL \u201905)","author":"S Lerner","year":"2005","unstructured":"Lerner S, Millstein T, Rice E, Chambers C (2005) Automated soundness proofs for dataflow analyses and transformations via local rules. In: Principles of programming languages (POPL \u201905). ACM Press, New York"},{"key":"108_CR26","volume-title":"Software engineering and formal methods (SEFM \u201905)","author":"D Leinenbach","year":"2005","unstructured":"Leinenbach D, Paul W, Petrova E (2005) Towards the formal verification of a C0 compiler: code generation and implementation correctness. In: Software engineering and formal methods (SEFM \u201905). IEEE Computer Society Press, Los Alamitos"},{"key":"108_CR27","series-title":"Mathematical aspects of computer science","first-page":"33","volume-title":"Applied mathematics","author":"J McCarthy","year":"1967","unstructured":"McCarthy J, Painter J (1967) Correctness of a compiler for arithmetic expressions. In: Applied mathematics. Mathematical aspects of computer science, vol 19. American Mathematical Society, Providence, pp 33\u201341"},{"issue":"4","key":"108_CR28","first-page":"461","volume":"5","author":"J Moore","year":"1989","unstructured":"Moore J (1989) A mechanically verified language implementation. J Autom Reason 5(4):461\u2013492","journal-title":"J Autom Reason"},{"key":"108_CR29","volume-title":"Piton: a mechanically verified assembly-level language","author":"J Moore","year":"1996","unstructured":"Moore J (1996) Piton: a mechanically verified assembly-level language. Kluwer Academic, Norwell"},{"key":"108_CR30","volume-title":"ACM symposium on principles of programming languages and systems","author":"GC Necula","year":"1997","unstructured":"Necula GC (1997) Proof-carrying code. In: ACM symposium on principles of programming languages and systems, Paris, France, January 1997"},{"key":"108_CR31","unstructured":"Necula GC (1998) Compiling with proofs. PhD thesis"},{"key":"108_CR32","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1145\/349299.349314","volume-title":"Programming language design and implementation (PLDI \u201900)","author":"GC Necula","year":"2000","unstructured":"Necula GC (2000) Translation validation for an optimizing compiler. In: Programming language design and implementation (PLDI \u201900). ACM Press, New York, pp 83\u201395"},{"key":"108_CR33","first-page":"333","volume-title":"Conference on programming language design and implementation (PLDI \u201900)","author":"GC Necula","year":"1998","unstructured":"Necula GC, Lee P (1998) The design and implementation of a certifying compiler. In: Conference on programming language design and implementation (PLDI \u201900). ACM Press, New York, pp 333\u2013344"},{"key":"108_CR34","series-title":"LNCS","volume-title":"Isabelle\/HOL\u2014a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL\u2014a proof assistant for higher-order logic. In: LNCS, vol 2283. Springer, Berlin"},{"key":"108_CR35","volume-title":"Computer organization and design, the hardware\/software interface","author":"DA Patterson","year":"1998","unstructured":"Patterson DA, Hennessy JL (1998) Computer organization and design, the hardware\/software interface, 2nd edn. Morgan Kaufmann, San Francisco","edition":"2"},{"issue":"1","key":"108_CR36","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/j.entcs.2005.03.023","volume":"132","author":"A Poetzsch-Heffter","year":"2005","unstructured":"Poetzsch-Heffter A, Gawkowski MJ (2005) Towards proof generating compilers. Electron Notes Theor Comput Sci 132(1):37\u201351","journal-title":"Electron Notes Theor Comput Sci"},{"key":"108_CR37","first-page":"151","volume-title":"LNCS","author":"A Pnueli","year":"1998","unstructured":"Pnueli A, Siegel M, Singerman E (1998) Translation validation. In: LNCS, vol 1384. Springer, Berlin, p\u00a0151"},{"key":"108_CR38","volume-title":"Run-time result verification","author":"M Rinard","year":"1999","unstructured":"Rinard M, Marinov D (1999) Credible compilation with pointers. In: Run-time result verification, Trento, Italy, July 1999. Springer, Berlin"},{"key":"108_CR39","unstructured":"Samet H (1975) Automatically proving the correctness of translations involving optimized code. PhD thesis, Computer Science Department, Stanford University"},{"key":"108_CR40","doi-asserted-by":"crossref","first-page":"492","DOI":"10.1145\/800191.805648","volume-title":"ACM 76: proceedings of the annual conference","author":"H Samet","year":"1976","unstructured":"Samet H (1976) Compiler testing via symbolic interpretation. In: ACM 76: proceedings of the annual conference. ACM Press, New York, pp 492\u2013497. http:\/\/doi.acm.org\/10.1145\/800191.805648"},{"key":"108_CR41","unstructured":"The Coq Development Team (2007) The Coq proof assistant reference manual\u2014version 8.1. http:\/\/coq.inria.fr"},{"key":"108_CR42","volume-title":"Principles of programming languages (POPL \u201908)","author":"J-B Tristan","year":"2008","unstructured":"Tristan J-B, Leroy X (2008) Formal verification of translation validators: a case study on instruction scheduling optimizations. In: Principles of programming languages (POPL \u201908). ACM Press, New York"},{"key":"108_CR43","volume-title":"Principles of programming languages (POPL \u201904)","author":"X Rival","year":"2004","unstructured":"Rival X (2004) Symbolic transfer functions-based approaches to certified compilation. In: Principles of programming languages (POPL \u201904). ACM Press, New York"},{"key":"108_CR44","series-title":"LNCS","volume-title":"Leveraging applications of formal methods","author":"W Zimmermann","year":"2006","unstructured":"Zimmermann W (2006) On the correctness of transformations in compiler back-ends. In: Leveraging applications of formal methods. LNCS, vol 4313. Springer, Berlin"},{"issue":"3","key":"108_CR45","first-page":"223","volume":"9","author":"L Zuck","year":"2003","unstructured":"Zuck L, Pnueli A, Fang Y, Goldberg B (2003) VOC: A methodology for the translation validation of optimizing compilers. J Univers Comput Sci 9(3):223\u2013247","journal-title":"J Univers Comput Sci"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0108-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-010-0108-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0108-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T06:07:15Z","timestamp":1559887635000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-010-0108-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,21]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,2]]}},"alternative-id":["108"],"URL":"https:\/\/doi.org\/10.1007\/s10703-010-0108-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12,21]]}}}