{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:28:56Z","timestamp":1750746536990},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2020,11]]},"DOI":"10.1007\/s11390-020-0536-9","type":"journal-article","created":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T11:11:43Z","timestamp":1607339503000},"page":"1382-1405","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Modular Verification of SPARCv8 Code"],"prefix":"10.1007","volume":"35","author":[{"given":"Jun-Peng","family":"Zha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xin-Yu","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":[[2020,11,30]]},"reference":[{"key":"536_CR1","doi-asserted-by":"crossref","unstructured":"Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z. A practical verification framework for preemptive OS kernels. In Proc. the 28th International Conference, July 2016, pp.59-79.","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"536_CR2","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 Proc. the 22nd ACM Symposium on Operating Systems Principles, Oct. 2009, pp.207-220.","DOI":"10.1145\/1629575.1629596"},{"key":"536_CR3","doi-asserted-by":"crossref","unstructured":"Gu R, Koenig J, Ramananandro T, Shao Z, Wu X N, Weng S C, Zhang H, Guo Y. Deep specifications and certified abstraction layers. In Proc. the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan. 2015, pp.59-5608.","DOI":"10.1145\/2676726.2676975"},{"key":"536_CR4","doi-asserted-by":"crossref","unstructured":"Zha J, Feng X, Qiao L. Modular verification of SPARCv8 code. In Proc. the 16th Asian Symposium on Programming Languages and Systems, December 2018, pp.245-263.","DOI":"10.1007\/978-3-030-02768-1_14"},{"key":"536_CR5","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 Proc. the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, June 2006, pp.401-414.","DOI":"10.1145\/1133255.1134028"},{"issue":"1","key":"536_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy X, Blazy S. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 2008, 41(1): 1-31.","journal-title":"Journal of Automated Reasoning"},{"key":"536_CR7","doi-asserted-by":"crossref","unstructured":"Wang J, Fu M, Qiao L, Feng X. Formalizing SPARCv8 instruction set architecture in Coq. In Proc. the 3rd International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, Oct. 2017, pp.300-316.","DOI":"10.1007\/978-3-319-69483-2_18"},{"key":"536_CR8","unstructured":"Reynolds J. Separation logic: A logic for shared mutable data structures. In Proc. the 17th IEEE Symposium on Logic in Computer Science, July 2002, pp.55-74."},{"key":"536_CR9","doi-asserted-by":"crossref","unstructured":"Liang H, Feng X, Shao Z. Compositional verification of termination-preserving refinement of concurrent programs. In Proc. the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM\/IEEE Symposium on Logic in Computer Science, July 2014, Article No. 65.","DOI":"10.1145\/2603088.2603123"},{"key":"536_CR10","doi-asserted-by":"crossref","unstructured":"Necula G C, Lee P. Safe kernel extensions without run-time checking. In Proc. the 2nd USENIX Symp. Operating System Design and Implementation, October 1996, pp.229-243.","DOI":"10.1145\/248155.238781"},{"key":"536_CR11","unstructured":"Appel A W. Foundational proof-carrying code. In Proc. the 16th Annual IEEE Symposium on Logic in Computer Science, June 1998, pp.247-256."},{"key":"536_CR12","unstructured":"Morrisett G, Crary K, Glew N, Grossman D, Samuels R, Smith F, Walker D, Weirich S, Zdancewic S. TALx86: A realistic typed assembly language. In Proc. the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, May 1996, pp.25-35."},{"key":"536_CR13","doi-asserted-by":"crossref","unstructured":"Morrisett G, Walker D, Crary K, Glew N. From system F to typed assembly language. In Proc. the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan. 1998, pp.85-97.","DOI":"10.1145\/268946.268954"},{"issue":"1\/2\/3","key":"536_CR14","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. Science of Computer Programming, 2004, 50(1\/2\/3): 101-127.","journal-title":"Science of Computer Programming"},{"key":"536_CR15","doi-asserted-by":"crossref","unstructured":"Ni Z, Shao Z. Certified assembly programming with embedded code pointers. In Proc. the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2006, pp.320-333.","DOI":"10.1145\/1111320.1111066"},{"key":"536_CR16","doi-asserted-by":"crossref","unstructured":"Tan G, Appel A W. A compositional logic for control flow. In Proc. the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan. 2006, pp.80-94.","DOI":"10.1007\/11609773_6"},{"key":"536_CR17","doi-asserted-by":"crossref","unstructured":"Myreen M O, Gordon M J. Hoare logic for realistically modelled machine code. In Proc. the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, March 2007, pp.568-582.","DOI":"10.1007\/978-3-540-71209-1_44"},{"key":"536_CR18","doi-asserted-by":"crossref","unstructured":"Hou Z, San\u00e1n 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 Proc. the 21st International Symposium on Formal Methods, November 2016, pp.388-405.","DOI":"10.1007\/978-3-319-48989-6_24"},{"key":"536_CR19","doi-asserted-by":"crossref","unstructured":"Ni Z, Yu D, Shao Z. Using XCAP to certify realistic systems code: Machine context management. In Proc. the 20th International Conference on Theorem Proving in Higher Order Logics, Sept. 2007, pp.189-206.","DOI":"10.1007\/978-3-540-74591-4_15"},{"key":"536_CR20","doi-asserted-by":"crossref","unstructured":"Yang J, Hawblitzel C. Safe to the last instruction: Automated verification of a type-safe operating system. In Proc. the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2010, pp.99-110.","DOI":"10.1145\/1809028.1806610"},{"key":"536_CR21","doi-asserted-by":"crossref","unstructured":"Berdine J, Calcagno C, O\u2019Hearn P W. Symbolic execution with separation logic. In Proc. the 3rd Asian Symposium on Programming Languages and Systems, November 2005, pp.52-68.","DOI":"10.1007\/11575467_5"},{"key":"536_CR22","doi-asserted-by":"crossref","unstructured":"Berdine J, Calcagno C, O\u2019Hearn P W. Smallfoot: Modular automatic assertion checking with separation logic. In Proc. the 4th International Symposium on Formal Methods for Components and Objects, November 2005, pp.115-137.","DOI":"10.1007\/11804192_6"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-020-0536-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-020-0536-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-020-0536-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T12:15:15Z","timestamp":1607343315000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-020-0536-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11]]},"references-count":22,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,11]]}},"alternative-id":["536"],"URL":"https:\/\/doi.org\/10.1007\/s11390-020-0536-9","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11]]},"assertion":[{"value":"11 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 October 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 November 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}