{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:56:27Z","timestamp":1743141387249,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319259413"},{"type":"electronic","value":"9783319259420"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25942-0_7","type":"book-chapter","created":{"date-parts":[[2015,10,16]],"date-time":"2015-10-16T05:32:14Z","timestamp":1444973534000},"page":"105-119","source":"Crossref","is-referenced-by-count":2,"title":["Towards Verified Faithful Simulation"],"prefix":"10.1007","author":[{"given":"Vania","family":"Joloboff","sequence":"first","affiliation":[]},{"given":"Jean-Fran\u00e7ois","family":"Monin","sequence":"additional","affiliation":[]},{"given":"Xiaomu","family":"Shi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,17]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Nardelli, F.Z.: The semantics of power and ARM multiprocessor machine code. In: DAMP 2009, pp. 13\u201324. ACM, New York (2008)","DOI":"10.1145\/1481839.1481842"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"7_CR3","first-page":"2011","volume":"53\u201364","author":"F Bobot","year":"2011","unstructured":"Bobot, F., Filli\u00e2tre, J., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. Boogie 53\u201364, 2011 (2011)","journal-title":"Boogie"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-35308-6_8","volume-title":"Certified Programs and Proofs","author":"B Campbell","year":"2012","unstructured":"Campbell, B.: An executable semantics for CompCert C. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 60\u201375. Springer, Heidelberg (2012)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Canet, G., Cuoq, P., Monate, B.: A value analysis for C programs. In: SCAM 2009, pp. 123\u2013124. IEEE (2009)","DOI":"10.1109\/SCAM.2009.22"},{"key":"7_CR6","unstructured":"Coq Development Team. The Coq Reference Manual, Version 8.2. INRIA Rocquencourt, France (2008). \n                      http:\/\/coq.inria.fr\/"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J-C Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The why\/krakatoa\/caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14052-5_18","volume-title":"Interactive Theorem Proving","author":"A Fox","year":"2010","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 243\u2013258. Springer, Heidelberg (2010)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Hao, H., Song, J., Helmstetter, C., Joloboff, V.: Generation of executable representation for processor simulation with dynamic translation. In: Proceedings of the International Conference on Computer Science and Software Engineering, Wuhan, China. IEEE (2008)","DOI":"10.1109\/CSSE.2008.635"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Helmstetter, C., Joloboff, V., Xiao, H.: SimSoC: a full system simulation software for embedded systems. In: IEEE (ed.) 2009 IEEE International Workshop on Open-source Software for Scientific Computation (OSSC), pp. 49\u201355, Sept 2009","DOI":"10.1109\/OSSC.2009.5416870"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: sel4: Formal verification of an os kernel. In: Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles, SOSP 2009, pp. 207\u2013220. ACM, New York (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"7","key":"7_CR12","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"7_CR13","unstructured":"Leroy, X.: The CompCert C verified compiler. Documentation and user\u2019s manual. INRIA Paris-Rocquencourt, March 2012"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-39634-2_25","volume-title":"Interactive Theorem Proving","author":"J-F Monin","year":"2013","unstructured":"Monin, J.-F., Shi, X.: Handcrafted inversions made operational on operational semantics. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 338\u2013353. Springer, Heidelberg (2013)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-49059-0_7","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"C Pusch","year":"1999","unstructured":"Pusch, C.: Proving the soundness of a java bytecode verifier specification in isabelle\/HOL. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 89. Springer, Heidelberg (1999)"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Sutarwala, S., Paulin, P.G., Kumar, Y.: Insulin: An instruction set simulation environment. In: CHDL 1993: 11th IFIP WG10.2 International Conference, pp. 369\u2013376. North-Holland, Amsterdam (1993)","DOI":"10.1016\/B978-0-444-81641-2.50034-4"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Witchel, E., Rosenblum, M.: Embra: fast and flexible machine simulation. In: SIGMETRICS 1996, pp. 68\u201379. ACM, New York (1996)","DOI":"10.1145\/233008.233025"},{"issue":"3","key":"7_CR18","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1109\/TVLSI.2002.1043339","volume":"10","author":"J Zhu","year":"2002","unstructured":"Zhu, J., Gajski, D.D.: An ultra-fast instruction set simulator. IEEE Trans. Very Large Scale Integr. Syst. 10(3), 363\u2013373 (2002)","journal-title":"IEEE Trans. Very Large Scale Integr. Syst."}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering: Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25942-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T02:54:00Z","timestamp":1559271240000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25942-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319259413","9783319259420"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25942-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}