{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,9]],"date-time":"2024-05-09T07:54:11Z","timestamp":1715241251316},"reference-count":19,"publisher":"World Scientific Pub Co Pte Ltd","issue":"04","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2003,8]]},"abstract":"<jats:p>This paper reports on a large verification effort in constructing an initial fully trusted bootstrap compiler executable for a realistic system programming language and real target processor. The construction and verification process comprises three tasks: the verification of the compiling specification (a relation between abstract source and target programs) with respect to the language semantics and a realistic correctness criterion. This proof has been completely mechanized using the PVS verification system and is one of the largest case-studies in formal verification we are aware of. Second, the implementation of the specification in the high-level source language following a transformational approach, and finally, the implementation and verification of a binary executable written in the compiler's target language. For the latter task, a realistic technique has been developed, which is based on rigorous a-posteriori syntactic code inspection and which guarantees, for the first time, trusted execution of generated machine programs. The context of this work is the joint German research effort Verifix aiming at developing methods for the construction of correct compilers for realistic source languages and real target processors.<\/jats:p>","DOI":"10.1142\/s0129054103001947","type":"journal-article","created":{"date-parts":[[2003,9,19]],"date-time":"2003-09-19T10:19:32Z","timestamp":1063966772000},"page":"659-680","source":"Crossref","is-referenced-by-count":10,"title":["A Completely Verified Realistic Bootstrap Compiler"],"prefix":"10.1142","volume":"14","author":[{"given":"Axel","family":"Dold","sequence":"first","affiliation":[{"name":"Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Ulm, James-Frank-Ring, D-89069 Ulm, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Friedrich von","family":"Henke","sequence":"additional","affiliation":[{"name":"Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Ulm, James-Frank-Ring, D-89069 Ulm, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Goerigk","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik und Praktische Mathematik, Universit\u00e4t Kiel, Olshausenstr. 40, D-24098 Kiel, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf5","doi-asserted-by":"publisher","DOI":"10.1145\/5397.30847"},{"key":"rf7","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383985"},{"key":"rf13","volume-title":"Computer Aided Reasoning: ACL2 Case Studies","author":"Goerigk W.","year":"2000"},{"key":"rf15","doi-asserted-by":"crossref","unstructured":"W.\u00a0Goerigk, T.\u00a0Gaul and W.\u00a0Zimmermann, Tool Support for System Specification, Development, and Verification, Advances in Computing Science, eds. R.\u00a0Berghammer and Y.\u00a0Lakhnech (Springer Verlag, Wien, New York, 1998)\u00a0pp. 108\u2013122.","DOI":"10.1007\/978-3-7091-6355-9_8"},{"key":"rf18","volume":"1","author":"Goerigk W.","journal-title":"International Journal on Problems of Programming"},{"key":"rf20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48092-7_10"},{"key":"rf21","volume-title":"Introduktion to HOL: A theorem proving environment for higher order logic","author":"Gordon M. J. C.","year":"1993"},{"key":"rf22","first-page":"264","volume":"43","author":"Gurevich Y.","journal-title":"Bulletin EATCS"},{"key":"rf23","volume-title":"Specification and Validation Methods","author":"Gurevich Y.","year":"1995"},{"key":"rf28","first-page":"251","volume":"13","author":"Langmaack H.","journal-title":"Real Time Systems"},{"key":"rf32","volume-title":"Piton: A Mechanically Verified Assembly-Level Language","author":"Moore J. S.","year":"1996"},{"key":"rf33","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027453"},{"key":"rf35","doi-asserted-by":"publisher","DOI":"10.1145\/358438.349314"},{"key":"rf36","volume-title":"Semantics with Applications : A Formal Introduction","author":"Nielson H. R.","year":"1992"},{"key":"rf37","doi-asserted-by":"publisher","DOI":"10.1109\/32.345827"},{"key":"rf38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61512-2"},{"key":"rf41","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10886-6"},{"key":"rf46","doi-asserted-by":"publisher","DOI":"10.1145\/358198.358210"},{"key":"rf47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-89543-1"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054103001947","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,26]],"date-time":"2023-04-26T23:32:47Z","timestamp":1682551967000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054103001947"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":19,"journal-issue":{"issue":"04","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2003,8]]}},"alternative-id":["10.1142\/S0129054103001947"],"URL":"https:\/\/doi.org\/10.1142\/s0129054103001947","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}