{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:53:03Z","timestamp":1740099183594,"version":"3.37.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030027674"},{"type":"electronic","value":"9783030027681"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","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":[[2018]]},"DOI":"10.1007\/978-3-030-02768-1_14","type":"book-chapter","created":{"date-parts":[[2018,10,21]],"date-time":"2018-10-21T07:42:27Z","timestamp":1540107747000},"page":"245-263","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Modular Verification of SPARCv8 Code"],"prefix":"10.1007","author":[{"given":"Junpeng","family":"Zha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Qiao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,22]]},"reference":[{"key":"14_CR1","unstructured":"Program logic for SPARCv8 implementation in Coq (project code). https:\/\/github.com\/jpzha\/VeriSparc"},{"key":"14_CR2","unstructured":"SPARC. https:\/\/gaisler.com\/doc\/sparcv8.pdf"},{"key":"14_CR3","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Proceedings of 16th Annual IEEE Symposium on Logic in Computer Science, pp. 85\u201397, January 1998"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115\u2013137. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_6"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11575467_5"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: TLDI, pp. 67\u201378 (2007)","DOI":"10.1145\/1190315.1190325"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: PLDI, June 2006","DOI":"10.1145\/1133981.1134028"},{"issue":"1","key":"14_CR8","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1145\/2775051.2676975","volume":"50","author":"Ronghui Gu","year":"2015","unstructured":"Gu, R., et al.: Deep specifications and certified abstraction layers. In: POPL, pp. 595\u2013608, January 2015","journal-title":"ACM SIGPLAN Notices"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: SOSP, pp. 207\u2013220, October 2009","DOI":"10.1145\/1629575.1629596"},{"key":"14_CR10","unstructured":"Morrisett, G.: TALx86: a realistic typed assembly language. In: 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pp. 25\u201335, May 1996"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. In: POPL, pp. 85\u201397, January 1998","DOI":"10.21236\/ADA358572"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-540-71209-1_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MO Myreen","year":"2007","unstructured":"Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 568\u2013582. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_44"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: Safe kernel extensions without run-time checking. In: Proceedings of 2nd USENIX Symposium on Operating System Design and Implementation, pp. 229\u2013243 (1996)","DOI":"10.1145\/238721.238781"},{"issue":"1","key":"14_CR14","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1145\/1111320.1111066","volume":"41","author":"Zhaozhong Ni","year":"2006","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: POPL, pp. 320\u2013333 (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-74591-4_15","volume-title":"Theorem Proving in Higher Order Logics","author":"Z Ni","year":"2007","unstructured":"Ni, Z., Yu, D., Shao, Z.: Using XCAP to certify realistic systems code: machine context management. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 189\u2013206. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74591-4_15"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/11609773_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G Tan","year":"2005","unstructured":"Tan, G., Appel, A.W.: A compositional logic for control flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 80\u201394. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_6"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-319-69483-2_18","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"J Wang","year":"2017","unstructured":"Wang, J., Fu, M., Qiao, L., Feng, X.: Formalizing SPARCv8 instruction set architecture in Coq. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 300\u2013316. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_18"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-319-41540-6_4","volume-title":"Computer Aided Verification","author":"F Xu","year":"2016","unstructured":"Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 59\u201379. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_4"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: PLDI, pp. 99\u2013110 (2010)","DOI":"10.1145\/1809028.1806610"},{"issue":"1\u20133","key":"14_CR20","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.scico.2004.01.003","volume":"50","author":"D Yu","year":"2004","unstructured":"Yu, D., Nadeem, A.H., Shao, Z.: Building certified libraries for PCC: dynamic storage allocation. Sci. Comput. Program. 50(1\u20133), 101\u2013127 (2004)","journal-title":"Sci. Comput. Program."},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-319-48989-6_24","volume-title":"FM 2016: Formal Methods","author":"Z Hou","year":"2016","unstructured":"Hou, Z., Sanan, D., Tiu, A., Liu, Y., Hoa, K.C.: An executable formalisation of the SPARCv8 instruction set architecture: a case study for the LEON3 processor. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 388\u2013405. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_24"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02768-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,27]],"date-time":"2019-10-27T06:11:27Z","timestamp":1572156687000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02768-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030027674","9783030027681"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02768-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Wellington","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Zealand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/aplas2018.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}