{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:06Z","timestamp":1750306746743,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,11,3]],"date-time":"2013-11-03T00:00:00Z","timestamp":1383436800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000935","name":"Department of Broadband, Communications and the Digital Economy , Australian Government","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000935","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,11,3]]},"DOI":"10.1145\/2525528.2525535","type":"proceedings-article","created":{"date-parts":[[2013,10,17]],"date-time":"2013-10-17T12:23:54Z","timestamp":1382012634000},"page":"1-7","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Towards a verified component platform"],"prefix":"10.1145","author":[{"given":"Matthew","family":"Fernandez","sequence":"first","affiliation":[{"name":"NICTA and the University of New South Wales, Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ihor","family":"Kuz","sequence":"additional","affiliation":[{"name":"NICTA and the University of New South Wales, Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[{"name":"NICTA and the University of New South Wales, Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[{"name":"NICTA and the University of New South Wales, Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,11,3]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/949344.949378"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1504\/IJES.2006.014859"},{"key":"e_1_3_2_1_3_1","volume-title":"5th SSV","author":"Andronick J.","year":"2010","unstructured":"J. Andronick , D. Greenaway , and K. Elphinstone . Towards proving security in the presence of large untrusted components. In G. Klein, R. Huuck, and B. Schlich, editors , 5th SSV , Vancouver, Canada , Oct 2010 . USENIX. J. Andronick, D. Greenaway, and K. Elphinstone. Towards proving security in the presence of large untrusted components. In G. Klein, R. Huuck, and B. Schlich, editors, 5th SSV, Vancouver, Canada, Oct 2010. USENIX."},{"key":"e_1_3_2_1_4_1","volume-title":"Formally verified system initialisation","author":"Boyton A.","year":"2013","unstructured":"A. Boyton , J. Andronick , C. Bannister , M. Fernandez , X. Gao , D. Greenaway , G. Klein , C. Lewis , and T. Sewell . Formally verified system initialisation . In Lindsay Groves, Jing Sun, editor, 15th ICFEM, Queenstown, New Zealand, Oct 2013 . Springer . A. Boyton, J. Andronick, C. Bannister, M. Fernandez, X. Gao, D. Greenaway, G. Klein, C. Lewis, and T. Sewell. Formally verified system initialisation. In Lindsay Groves, Jing Sun, editor, 15th ICFEM, Queenstown, New Zealand, Oct 2013. Springer."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2006.888386"},{"key":"e_1_3_2_1_6_1","first-page":"74","volume-title":"VSTTE 2005","author":"Fisler K.","year":"2005","unstructured":"K. Fisler and S. Krishnamurthi . Decomposing verification around end-user features . In VSTTE 2005 , pages 74 -- 81 . Springer , Oct 2005 . K. Fisler and S. Krishnamurthi. Decomposing verification around end-user features. In VSTTE 2005, pages 74--81. Springer, Oct 2005."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/786769.787035"},{"key":"e_1_3_2_1_8_1","unstructured":"D.\n      Greenaway J.\n      Andronick and \n      G.\n      Klein\n  . \n  Bridging the gap: Automatic verified abstraction of C\n  . In L. Beringer and A. Felty editors 3rd ITP volume \n  7406\n   of \n  LNCS pages \n  99\n  --\n  115 Princeton New Jersey Aug \n  2012\n  . \n  Springer\n  . ISBN 978-3-642-32346-1.  D. Greenaway J. Andronick and G. Klein. Bridging the gap: Automatic verified abstraction of C. In L. Beringer and A. Felty editors 3rd ITP volume 7406 of LNCS pages 99--115 Princeton New Jersey Aug 2012. Springer. ISBN 978-3-642-32346-1."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133572.1133615"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2006.08.039"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1851276.1851284"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/978-3-540-40007-3_11","volume-title":"Formal Methods at the Crossroads: from Panacea to Foundational Support","author":"Moore J. S.","year":"2003","unstructured":"J. S. Moore . A grand challenge for formal methods: A verified stack . In B. K. Aichernig and T. Maibaum, editors, Formal Methods at the Crossroads: from Panacea to Foundational Support , pages 161 -- 172 . Springer , 2003 . J. S. Moore. A grand challenge for formal methods: A verified stack. In B. K. Aichernig and T. Maibaum, editors, Formal Methods at the Crossroads: from Panacea to Foundational Support, pages 161--172. Springer, 2003."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_18_1","series-title":"LNCS","volume-title":"Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. Paulson , and M. Wenzel . Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS . Springer , 2002 . T. Nipkow, L. Paulson, and M. Wenzel. Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1049404"},{"key":"e_1_3_2_1_20_1","first-page":"151","volume-title":"4th TACAS","author":"Pnueli A.","year":"1998","unstructured":"A. Pnueli , M. Siegel , and E. Singerman . Translation validation . In 4th TACAS , pages 151 -- 166 , Lisbon, Portugal, Mar 1998 . Springer . A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In 4th TACAS, pages 151--166, Lisbon, Portugal, Mar 1998. Springer."},{"key":"e_1_3_2_1_21_1","first-page":"294","volume-title":"Proceedings of 7th DoD\/NBS Computer Security Conference","author":"Rushby J.","year":"1984","unstructured":"J. Rushby . A trusted computing base for embedded systems . In Proceedings of 7th DoD\/NBS Computer Security Conference , pages 294 -- 311 , Sep 1984 . J. Rushby. A trusted computing base for embedded systems. In Proceedings of 7th DoD\/NBS Computer Security Conference, pages 294--311, Sep 1984."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/800216.806586"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"T.\n      Sewell S.\n      Winwood P.\n      Gammie T.\n      Murray J.\n      Andronick and \n      G.\n      Klein\n  . \n  seL4 enforces integrity\n  . In M. C. J. D. van Eekelen H. Geuvers J. Schmaltz and F. Wiedijk editors 2nd ITP volume \n  6898\n   of \n  LNCS pages \n  325\n  --\n  340 Nijmegen The Netherlands Aug \n  2011\n  . \n  Springer\n  . doi: http:\/\/dx.doi.org\/10.1007\/978-3-642-22863-6_24.     10.1007\/978-3-642-22863-6_24\nT. Sewell S. Winwood P. Gammie T. Murray J. Andronick and G. Klein. seL4 enforces integrity. In M. C. J. D. van Eekelen H. Geuvers J. Schmaltz and F. Wiedijk editors 2nd ITP volume 6898 of LNCS pages 325--340 Nijmegen The Netherlands Aug 2011. Springer. doi: http:\/\/dx.doi.org\/10.1007\/978-3-642-22863-6_24.","DOI":"10.1007\/978-3-642-22863-6_24"},{"key":"e_1_3_2_1_24_1","volume-title":"Component Software: Beyond Object-Oriented Programming","author":"Szyperski C.","year":"1997","unstructured":"C. Szyperski . Component Software: Beyond Object-Oriented Programming . Addison-Wesley\/ACM Press , Essex, England , 1997 . C. Szyperski. Component Software: Beyond Object-Oriented Programming. Addison-Wesley\/ACM Press, Essex, England, 1997."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244801"}],"event":{"name":"SOSP '13: ACM SIGOPS 24th Symposium on Operating Systems Principles","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Farmington Pennsylvania","acronym":"SOSP '13"},"container-title":["Proceedings of the Seventh Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2525528.2525535","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2525528.2525535","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:24Z","timestamp":1750231704000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2525528.2525535"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11,3]]},"references-count":26,"alternative-id":["10.1145\/2525528.2525535","10.1145\/2525528"],"URL":"https:\/\/doi.org\/10.1145\/2525528.2525535","relation":{},"subject":[],"published":{"date-parts":[[2013,11,3]]},"assertion":[{"value":"2013-11-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}