{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T19:08:56Z","timestamp":1743016136994,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319489889"},{"type":"electronic","value":"9783319489896"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-48989-6_24","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T01:31:19Z","timestamp":1478482279000},"page":"388-405","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor"],"prefix":"10.1007","author":[{"given":"Zhe","family":"Hou","sequence":"first","affiliation":[]},{"given":"David","family":"Sanan","sequence":"additional","affiliation":[]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Koh Chuen","family":"Hoa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"24_CR1","unstructured":"ESA LEON processor. http:\/\/www.esa.int\/Our_Activities\/Space_Engineering_Technology\/LEON_the_space_chip_that_Europe_built . Accessed 27 Jan 2016"},{"key":"24_CR2","unstructured":"K computer. http:\/\/www.top500.org\/system\/177232 . Accessed 27 Jan 2016"},{"key":"24_CR3","unstructured":"L3 specification language for ISAs. http:\/\/www.cl.cam.ac.uk\/~acjf3\/l3\/ . Accessed 09 Dec 2015"},{"key":"24_CR4","unstructured":"LEON3 processor. http:\/\/www.gaisler.com\/index.php\/products\/processors\/leon3 . Accessed 27 Oct 2015"},{"key":"24_CR5","unstructured":"RISC-V architecture. https:\/\/riscv.org\/ . Accessed 10 Aug 2016"},{"key":"24_CR6","unstructured":"Securify: micro-kernel verification. http:\/\/securify.scse.ntu.edu.sg\/MicroVer\/ . Accessed 24 May 2016"},{"key":"24_CR7","unstructured":"The SPARC architecture manual version 8. http:\/\/gaisler.com\/doc\/sparcv8.pdf . Accessed 27 Oct 2015"},{"key":"24_CR8","unstructured":"Tianhe-2. http:\/\/top500.org\/system\/177999 . Accessed 27 Jan 2016"},{"key":"24_CR9","unstructured":"Xtratum hypervisor. http:\/\/www.xtratum.org\/ . Accessed 29 Jan 2016"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-68103-8_2","volume-title":"Types for Proofs and Programs","author":"R Atkey","year":"2008","unstructured":"Atkey, R.: CoqJVM: an executable specification of the java virtual machine using dependent types. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 18\u201332. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-68103-8_2"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-319-10702-8_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"B Campbell","year":"2014","unstructured":"Campbell, B., Stark, I.: Randomised testing of a microprocessor model using SMT-solver state generation. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 185\u2013199. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-10702-8_13"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167\u2013182. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71067-7_16"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"El Kady, S., Khater, M., Alhafnawi, M.: MIPS, ARM and SPARC-an architecture comparison. In: Proceedings of the World Congress on Engineering, vol. 1 (2014)","DOI":"10.21608\/iccae.2014.44094"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10930755_2","volume-title":"Theorem Proving in Higher Order Logics","author":"A Fox","year":"2003","unstructured":"Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25\u201340. Springer, Heidelberg (2003). doi: 10.1007\/10930755_2"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-32347-8_23","volume-title":"Interactive Theorem Proving","author":"A Fox","year":"2012","unstructured":"Fox, A.: Directions in ISA specification. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 338\u2013344. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32347-8_23"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-22102-1_12","volume-title":"Interactive Theorem Proving","author":"A Fox","year":"2015","unstructured":"Fox, A.: Improved tool support for machine-code decompilation in HOL4. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 187\u2013202. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-22102-1_12"},{"key":"24_CR17","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). doi: 10.1007\/978-3-642-14052-5_18"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Goel, S., Hunt, W.A., Kaufmann, M.: Abstract stobjs and their application to ISA modeling. In: ACL2 2013, pp. 54\u201369 (2013)","DOI":"10.4204\/EPTCS.114.5"},{"key":"24_CR19","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP 1983, pp. 321\u2013332. North-Holland (1983)"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-319-03545-1_18","volume-title":"Certified Programs and Proofs","author":"N Khakpour","year":"2013","unstructured":"Khakpour, N., Schwarz, O., Dam, M.: Machine assisted proof of ARMv7 instruction level isolation properties. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 276\u2013291. Springer, Heidelberg (2013). doi: 10.1007\/978-3-319-03545-1_18"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proceedings of the 33rd ACM Symposium on Principles of Programming Languages (2006)","DOI":"10.1145\/1111037.1111042"},{"key":"24_CR22","unstructured":"Leroy, X.: The CompCert C verified compiler (2015). http:\/\/compcert.inria.fr\/man\/manual.pdf . Accessed 29 Jan 2016"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Liu, H., Moore, J.S.: Executable JVM model for analytical reasoning: a study. In: Proceedings of the 2003 Workshop on Interpreters, Virtual Machines and Emulators, pp. 15\u201323. ACM (2003)","DOI":"10.1145\/858570.858572"},{"key":"24_CR24","unstructured":"Santoro, A., Park, W., Luckham, D.: SPARC-V9 architecture specification with Rapide. Technical report, Stanford, CA, USA (1995)"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-CC multiprocessor machine code. In: Proceedings of the 36th Annual ACM Symposium on Principles of Programming Languages, pp. 379\u2013391. ACM (2009)","DOI":"10.1145\/1594834.1480929"},{"key":"24_CR26","series-title":"Advances in Information Security","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-0-387-44599-1_13","volume-title":"Malware Detection","author":"G Smith","year":"2007","unstructured":"Smith, G.: Principles of secure information flow analysis. In: Christodorescu, M., Jha, S., Maughan, D., Song, D., Wang, C. (eds.) Malware Detection. Advances in Information Security, vol. 27, pp. 291\u2013307. Springer, Heidelberg (2007). doi: 10.1007\/978-0-387-44599-1_13"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"791","DOI":"10.1007\/978-3-662-49674-9_50","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Zhao","year":"2016","unstructured":"Zhao, Y., San\u00e1n, D., Zhang, F., Liu, Y.: Reasoning about information flow security of separation Kernels with channel-based communication. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 791\u2013810. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_50"}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,15]],"date-time":"2019-09-15T05:54:23Z","timestamp":1568526863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 November 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fm2016.cs.ucy.ac.cy\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}