{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T09:17:38Z","timestamp":1780996658082,"version":"3.54.1"},"reference-count":10,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2010,6,1]],"date-time":"2010-06-01T00:00:00Z","timestamp":1275350400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2010,6]]},"DOI":"10.1145\/1743546.1743574","type":"journal-article","created":{"date-parts":[[2010,6,1]],"date-time":"2010-06-01T12:21:35Z","timestamp":1275394895000},"page":"107-115","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":227,"title":["seL4"],"prefix":"10.1145","volume":"53","author":[{"given":"Gerwin","family":"Klein","sequence":"first","affiliation":[{"name":"National ICT Australia (NICTA), University of South Wales (UNSW), Sydney"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[{"name":"NICTA, UNSW"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kevin","family":"Elphinstone","sequence":"additional","affiliation":[{"name":"NICTA, UNSW"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"NICTA, UNSW, Open Kernel Labs"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Cock","sequence":"additional","affiliation":[{"name":"NICTA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philip","family":"Derrin","sequence":"additional","affiliation":[{"name":"NICTA, now at Open Kernel Labs"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dhammika","family":"Elkaduwe","sequence":"additional","affiliation":[{"name":"NICTA, UNSW, now at University of Peradeniya, Sri Lanka"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kai","family":"Engelhardt","sequence":"additional","affiliation":[{"name":"NICTA, UNSW"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rafal","family":"Kolanski","sequence":"additional","affiliation":[{"name":"NICTA, UNSW"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[{"name":"NICTA, Australian National University, Canberra"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[{"name":"NICTA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Harvey","family":"Tuch","sequence":"additional","affiliation":[{"name":"NICTA, UNSW, now at VMWare"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simon","family":"Winwood","sequence":"additional","affiliation":[{"name":"NICTA, UNSW"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Formal pervasive verification of a paging mechanism","author":"Alkassar E.","year":"2008","unstructured":"Alkassar , E. , Schirmer , N. , Starostin , A. Formal pervasive verification of a paging mechanism . TACAS. C.R. Ramakrishnan and J. Rehof, eds. Volume 4963 of LNCS ( 2008 ). Springer , 109--123. Alkassar, E., Schirmer, N., Starostin, A. Formal pervasive verification of a paging mechanism. TACAS. C.R. Ramakrishnan and J. Rehof, eds. Volume 4963 of LNCS (2008). Springer, 109--123."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_11"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/234215.234473"},{"key":"e_1_2_1_7_1","series-title":"LNCS (Kaiserslautern","volume-title":"Using XCAP to certify realistic system code: Machine context management. 20th TPHOLs","author":"Ni Z.","year":"2007","unstructured":"Ni , Z. , Yu , D. , Shao . Z. Using XCAP to certify realistic system code: Machine context management. 20th TPHOLs , volume 4732 of LNCS (Kaiserslautern , Germany, Sept 2007 ), Springer , 189--206. Ni, Z., Yu, D., Shao. Z. Using XCAP to certify realistic system code: Machine context management. 20th TPHOLs, volume 4732 of LNCS (Kaiserslautern, Germany, Sept 2007), Springer, 189--206."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Nipkow T. Paulson L. Wenzel M.\n      Isabelle\n      \/\n      HOL---A\n      Proof Assistant\n     for Higher-Order Logic.\n   Volume \n  2283\n   of \n  LNCS (2002) Springer\n  .   Nipkow T. Paulson L. Wenzel M. Isabelle\/HOL---A Proof Assistant for Higher-Order Logic . Volume 2283 of LNCS (2002) Springer.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_9_1","unstructured":"Ormandy T. Tinnes J. Linux null pointer dereference due to incorrect proto_ops initializations. http:\/\/www.cr0.org\/misc\/CVE-2009-2692.txt 2009.  Ormandy T. Tinnes J. Linux null pointer dereference due to incorrect proto_ops initializations. http:\/\/www.cr0.org\/misc\/CVE-2009-2692.txt 2009."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1975.9939"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/319151.319163"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1743546.1743574","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1743546.1743574","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:23:19Z","timestamp":1750245799000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1743546.1743574"}},"subtitle":["formal verification of an operating-system kernel"],"short-title":[],"issued":{"date-parts":[[2010,6]]},"references-count":10,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2010,6]]}},"alternative-id":["10.1145\/1743546.1743574"],"URL":"https:\/\/doi.org\/10.1145\/1743546.1743574","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,6]]},"assertion":[{"value":"2010-06-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}