{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T16:22:21Z","timestamp":1792254141421,"version":"4.4.0"},"reference-count":134,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,1]],"date-time":"2014-02-01T00:00:00Z","timestamp":1391212800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"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"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Syst."],"published-print":{"date-parts":[[2014,2]]},"abstract":"<jats:p>We present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel.<\/jats:p>\n                  <jats:p>We discuss the kernel design we used to make its verification tractable. We then describe the functional correctness proof of the kernel's C implementation and we cover further steps that transform this result into a comprehensive formal verification of the kernel: a formally verified IPC fastpath, a proof that the binary code of the kernel correctly implements the C semantics, a proof of correct access-control enforcement, a proof of information-flow noninterference, a sound worst-case execution time analysis of the binary, and an automatic initialiser for user-level systems that connects kernel-level access-control enforcement with reasoning about system behaviour. We summarise these results and show how they integrate to form a coherent overall analysis, backed by machine-checked, end-to-end theorems.<\/jats:p>\n                  <jats:p>The seL4 microkernel is currently not just the only general-purpose operating system kernel that is fully formally verified to this degree. It is also the only example of formal proof of this scale that is kept current as the requirements, design and implementation of the system evolve over almost a decade. We report on our experience in maintaining this evolving formally verified code base.<\/jats:p>","DOI":"10.1145\/2560537","type":"journal-article","created":{"date-parts":[[2014,2,25]],"date-time":"2014-02-25T08:20:45Z","timestamp":1393316445000},"page":"1-70","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":268,"title":["Comprehensive formal verification of an OS microkernel"],"prefix":"10.1145","volume":"32","author":[{"given":"Gerwin","family":"Klein","sequence":"first","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kevin","family":"Elphinstone","sequence":"additional","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rafal","family":"Kolanski","sequence":"additional","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,2,26]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the Summer USENIX Technical Conference. USENIX Association, 93--112","author":"Accetta M.","unstructured":"M. Accetta , R. Baron , W. Bolosky , D. Golub , R. Rashid , A. Tevanian , and M. Young . 1986. Mach: A new kernel foundation for UNIX development . In Proceedings of the Summer USENIX Technical Conference. USENIX Association, 93--112 . M. Accetta, R. Baron, W. Bolosky, D. Golub, R. Rashid, A. Tevanian, and M. Young. 1986. Mach: A new kernel foundation for UNIX development. In Proceedings of the Summer USENIX Technical Conference. USENIX Association, 93--112."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the Conference on Formal Methods in Computer-Aided Design. R. Bloem and N. Sharygina, Eds., IEEE, 267--270","author":"Alkassar E.","unstructured":"E. Alkassar , E. Cohen , M. A. Hillebrand , M. Kovalev , and W. Paul . 2010a. Verifying shadow page table algorithms . In Proceedings of the Conference on Formal Methods in Computer-Aided Design. R. Bloem and N. Sharygina, Eds., IEEE, 267--270 . E. Alkassar, E. Cohen, M. A. Hillebrand, M. Kovalev, and W. Paul. 2010a. Verifying shadow page table algorithms. In Proceedings of the Conference on Formal Methods in Computer-Aided Design. R. Bloem and N. Sharygina, Eds., IEEE, 267--270."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9123-z"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"E. Alkassar M. Hillebrand W. Paul and E. Petrova . 2010 b. Automated verification of a small hypervisor. In Proceedings of Verified Software: Theories Tools and Experiments. G. Leavens P. O'Hearn and S. Rajamani Eds. Lecture Notes in Computer Science vol. 6217 Springer 40--54. E. Alkassar M. Hillebrand W. Paul and E. Petrova. 2010b. Automated verification of a small hypervisor. In Proceedings of Verified Software: Theories Tools and Experiments. G. Leavens P. O'Hearn and S. Rajamani Eds. Lecture Notes in Computer Science vol. 6217 Springer 40--54.","DOI":"10.1007\/978-3-642-15057-9_3"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"E. Alkassar W. Paul A. Starostin and A. Tsyban . 2010 c. Pervasive verification of an OS microkernel: Inline assembly memory consumption concurrent devices. In Proceedings of Verified Software: Theories Tools and Experiments. P. O'Hearn G. T. Leavens and S. Rajamani Eds. Lecture Notes in Computer Science vol. 6217 Springer 71--85. E. Alkassar W. Paul A. Starostin and A. Tsyban. 2010c. Pervasive verification of an OS microkernel: Inline assembly memory consumption concurrent devices. In Proceedings of Verified Software: Theories Tools and Experiments. P. O'Hearn G. T. Leavens and S. Rajamani Eds. Lecture Notes in Computer Science vol. 6217 Springer 71--85.","DOI":"10.1007\/978-3-642-15057-9_5"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"E. Alkassar N. Schirmer and A. Starostin . 2008 . Formal pervasive verification of a paging mechanism. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). C. R. Ramakrishnan and J. Rehof Eds. Lecture Notes in Computer Science vol. 4963 Springer 109--123. E. Alkassar N. Schirmer and A. Starostin. 2008. Formal pervasive verification of a paging mechanism. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). C. R. Ramakrishnan and J. Rehof Eds. Lecture Notes in Computer Science vol. 4963 Springer 109--123.","DOI":"10.1007\/978-3-540-78800-3_9"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1504\/IJES.2006.014859"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 5th Systems Software Verification. G. Klein, R. Huuck, and B. Schlich, Eds., USENIX","author":"Andronick J.","unstructured":"J. Andronick , D. Greenaway , and K. Elphinstone . 2010. Towards proving security in the presence of large untrusted components . In Proceedings of the 5th Systems Software Verification. G. Klein, R. Huuck, and B. Schlich, Eds., USENIX , Berkeley, CA. J. Andronick, D. Greenaway, and K. Elphinstone. 2010. Towards proving security in the presence of large untrusted components. In Proceedings of the 5th Systems Software Verification. G. Klein, R. Huuck, and B. Schlich, Eds., USENIX, Berkeley, CA."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the International Conference on Software Engineering. ACM, 1002--1011","author":"Andronick J.","unstructured":"J. Andronick , R. Jeffery , G. Klein , R. Kolanski , M. Staples , H. J. Zhang , and L. Zhu . 2012. Large-scale formal verification in practice: A process perspective . In Proceedings of the International Conference on Software Engineering. ACM, 1002--1011 . J. Andronick, R. Jeffery, G. Klein, R. Kolanski, M. Staples, H. J. Zhang, and L. Zhu. 2012. Large-scale formal verification in practice: A process perspective. In Proceedings of the International Conference on Software Engineering. ACM, 1002--1011."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 4th IEEE Workshop on Policies for Distributed Systems and Networks (POLICY). IEEE, 158--169","author":"Archer M.","unstructured":"M. Archer , E. Leonard , and M. Pradella . 2003. Analyzing security-enhanced Linux policy specifications . In Proceedings of the 4th IEEE Workshop on Policies for Distributed Systems and Networks (POLICY). IEEE, 158--169 . M. Archer, E. Leonard, and M. Pradella. 2003. Analyzing security-enhanced Linux policy specifications. In Proceedings of the 4th IEEE Workshop on Policies for Distributed Systems and Networks (POLICY). IEEE, 158--169."},{"key":"e_1_2_1_11_1","volume-title":"ARM1136JF-S and ARM1136J-S Technical Reference Manual. R1P1 Ed","author":"Ltd ARM","unstructured":"ARM Ltd . 2005. ARM1136JF-S and ARM1136J-S Technical Reference Manual. R1P1 Ed ., ARM Ltd . ARM Ltd. 2005. ARM1136JF-S and ARM1136J-S Technical Reference Manual. R1P1 Ed., ARM Ltd."},{"key":"e_1_2_1_12_1","volume-title":"SLIC: A specification language for interface checking. Tech. Rep. MSR-TR-2001-21, Microsoft Research.","author":"Ball T.","year":"2001","unstructured":"T. Ball and S. K. Rajamani . 2001 . SLIC: A specification language for interface checking. Tech. Rep. MSR-TR-2001-21, Microsoft Research. T. Ball and S. K. Rajamani. 2001. SLIC: A specification language for interface checking. Tech. Rep. MSR-TR-2001-21, Microsoft Research."},{"key":"e_1_2_1_13_1","unstructured":"J. Barhorst T. Belote P. Binns J. Hoffman J. Paunicka P. Sarathy J. Scoredos P. Stanfill D. Stuart and R. Urzi. 2009. A research agenda for mixed-criticality systems. http:\/\/www.cse.wustl.edu\/&sim;cdgill\/CPSWEEK09_MCAR\/. J. Barhorst T. Belote P. Binns J. Hoffman J. Paunicka P. Sarathy J. Scoredos P. Stanfill D. Stuart and R. Urzi. 2009. A research agenda for mixed-criticality systems. http:\/\/www.cse.wustl.edu\/&sim;cdgill\/CPSWEEK09_MCAR\/."},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"G. Barthe G. Betarte J. D. Campo and C. Luna . 2011 . Formally verifying isolation and availability in an idealized model of virtualization. In Proceedings of the 17th International Symposium on Formal Methods (FM). M. Butler and W. Schulte Eds. Lecture Notes in Computer Science vol. 6664 Springer 231--245. G. Barthe G. Betarte J. D. Campo and C. Luna. 2011. Formally verifying isolation and availability in an idealized model of virtualization. In Proceedings of the 17th International Symposium on Formal Methods (FM). M. Butler and W. Schulte Eds. Lecture Notes in Computer Science vol. 6664 Springer 231--245.","DOI":"10.1007\/978-3-642-21437-0_19"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.17"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224077"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.41331"},{"key":"e_1_2_1_20_1","volume-title":"Tech. Rep. 89","author":"Bevier W. R.","year":"1993","unstructured":"W. R. Bevier and L. Smith . 1993 . A mathematical model of the Mach kernel: Atomic actions and locks. Tech. Rep. 89 , Computational Logic Inc . Apr. W. R. Bevier and L. Smith. 1993. A mathematical model of the Mach kernel: Atomic actions and locks. Tech. Rep. 89, Computational Logic Inc. Apr."},{"key":"e_1_2_1_21_1","volume-title":"Computer Security: Art and Science","author":"Bishop M.","unstructured":"M. Bishop . 2003. Computer Security: Art and Science . Addison-Wesley . M. Bishop. 2003. Computer Security: Art and Science. Addison-Wesley."},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"B. Blackham and G. Heiser. 2012. Correct fast maintainable -- choose any three&excl; In Proceedings of the 3rd Asia-Pacific Workshop on Systems (APSys). 13:1--13:7. B. Blackham and G. Heiser. 2012. Correct fast maintainable -- choose any three&excl; In Proceedings of the 3rd Asia-Pacific Workshop on Systems (APSys). 13:1--13:7.","DOI":"10.1145\/2349896.2349909"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2013.6531083"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2168836.2168869"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2349896.2349904"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302691"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 15th International Conference on Formal Engineering Methods. Lindsay Groves and Jing Sun, Ed., Springer, 70--85","author":"Boyton A.","unstructured":"A. Boyton , J. Andronick , C. Bannister , M. Fernandez , X. Gao , D. Greenaway , G. Klein , C. Lewis , and T. Sewell . 2013. Formally verified system initialisation . In Proceedings of the 15th International Conference on Formal Engineering Methods. Lindsay Groves and Jing Sun, Ed., Springer, 70--85 . A. Boyton, J. Andronick, C. Bannister, M. Fernandez, X. Gao, D. Greenaway, G. Klein, C. Lewis, and T. Sewell. 2013. Formally verified system initialisation. In Proceedings of the 15th International Conference on Formal Engineering Methods. Lindsay Groves and Jing Sun, Ed., Springer, 70--85."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/362258.362278"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 2nd International Workshop on Real-Time Tools.","author":"Carlsson M.","unstructured":"M. Carlsson , J. Engblom , A. Ermedahl , J. Lindblad , and B. Lisper . 2002. Worst-case execution time analysis of disable interrupt regions in a commercial real-time operating system . In Proceedings of the 2nd International Workshop on Real-Time Tools. M. Carlsson, J. Engblom, A. Ermedahl, J. Lindblad, and B. Lisper. 2002. Worst-case execution time analysis of disable interrupt regions in a commercial real-time operating system. In Proceedings of the 2nd International Workshop on Real-Time Tools."},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 5th International Verification Workshop. B. Beckert and G. Klein, Eds., CEUR Workshop Proceedings","volume":"372","author":"Cock D.","year":"2008","unstructured":"D. Cock . 2008 . Bitfields and tagged unions in C: Verification through automatic generation . In Proceedings of the 5th International Verification Workshop. B. Beckert and G. Klein, Eds., CEUR Workshop Proceedings , vol. 372 , 44--55. D. Cock. 2008. Bitfields and tagged unions in C: Verification through automatic generation. In Proceedings of the 5th International Verification Workshop. B. Beckert and G. Klein, Eds., CEUR Workshop Proceedings, vol. 372, 44--55."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_28"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 13th Euromicro Conference on Real-Time Systems. 191--198","author":"Colin A.","unstructured":"A. Colin and I. Puaut . 2001. Worst case execution time analysis of the RTEMS real-time operating system . In Proceedings of the 13th Euromicro Conference on Real-Time Systems. 191--198 . A. Colin and I. Puaut. 2001. Worst case execution time analysis of the RTEMS real-time operating system. In Proceedings of the 13th Euromicro Conference on Real-Time Systems. 191--198."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_2_1_36_1","unstructured":"COYOTOS 2008. The Coyotos secure operating system. http:\/\/www.coyotos.org\/. COYOTOS 2008. The Coyotos secure operating system. http:\/\/www.coyotos.org\/."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294295"},{"key":"e_1_2_1_38_1","unstructured":"U. Dannowski. 2009. Personal communication. U. Dannowski. 2009. Personal communication."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0296-9"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science","volume":"4963","author":"de Moura L. M.","unstructured":"L. M. de Moura and N. Bj\u00f8rner . 2008. Z3: An efficient SMT solver . In Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science , vol. 4963 , Springer, Berlin, Germany, 337--340. L. M. de Moura and N. Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 4963, Springer, Berlin, Germany, 337--340."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/1525579"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2039239.2039245"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159842.1159850"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1435458.1435465"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522720"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the 11th Workshop on Hot Topics in Operating Systems. 117--122","author":"Elphinstone K.","unstructured":"K. Elphinstone , G. Klein , P. Derrin , T. Roscoe , and G. Heiser . 2007. Towards a practical, verified kernel . In Proceedings of the 11th Workshop on Hot Topics in Operating Systems. 117--122 . K. Elphinstone, G. Klein, P. Derrin, T. Roscoe, and G. Heiser. 2007. Towards a practical, verified kernel. In Proceedings of the 11th Workshop on Hot Topics in Operating Systems. 117--122."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217953"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the National Computer Conference, AFIPS Conference Proceedings. 329--334","author":"Feiertag R. J.","unstructured":"R. J. Feiertag and P. G. Neumann . 1979. The foundations of a provably secure operating system (PSOS) . In Proceedings of the National Computer Conference, AFIPS Conference Proceedings. 329--334 . R. J. Feiertag and P. G. Neumann. 1979. The foundations of a provably secure operating system (PSOS). In Proceedings of the National Computer Conference, AFIPS Conference Proceedings. 329--334."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 3rd USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, 101--115","author":"Ford B.","unstructured":"B. Ford , M. Hibler , J. Lepreau , R. McGrath , and P. Tullmann . 1999. Interface and execution models in the Fluke kernel . In Proceedings of the 3rd USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, 101--115 . B. Ford, M. Hibler, J. Lepreau, R. McGrath, and P. Tullmann. 1999. Interface and execution models in the Fluke kernel. In Proceedings of the 3rd USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, 101--115."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_2"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945464"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 11--20","author":"Goguen J.","unstructured":"J. Goguen and J. Meseguer . 1982. Security policies and security models . In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 11--20 . J. Goguen and J. Meseguer. 1982. Security policies and security models. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 11--20."},{"key":"e_1_2_1_56_1","volume-title":"Edinburgh LCF. Lecture Notes in Computer Science","volume":"78","author":"Gordon M. J. C.","unstructured":"M. J. C. Gordon , R. Milner , and C. P. Wadsworth . 1979 . Edinburgh LCF. Lecture Notes in Computer Science , vol. 78 , Springer. M. J. C. Gordon, R. Milner, and C. P. Wadsworth. 1979. Edinburgh LCF. Lecture Notes in Computer Science, vol. 78, Springer."},{"key":"e_1_2_1_57_1","unstructured":"Greenhills Software Inc. 2008. Integrity real-time operating system. http:\/\/www.ghs.com\/products\/rtos\/integrity.html. Greenhills Software Inc. 2008. Integrity real-time operating system. http:\/\/www.ghs.com\/products\/rtos\/integrity.html."},{"key":"e_1_2_1_58_1","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"Greve D. A.","unstructured":"D. A. Greve . 2010. Information security modeling and analysis . In Design and Verification of Microprocessor Systems for High-Assurance Applications , D. S. Hardin, Ed., Springer , 249--300. D. A. Greve. 2010. Information security modeling and analysis. In Design and Verification of Microprocessor Systems for High-Assurance Applications, D. S. Hardin, Ed., Springer, 249--300."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.5555\/1066473.1066478"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1987.226478"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217975.1217978"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/1700527.1700692"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180448"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.70772"},{"key":"e_1_2_1_65_1","volume-title":"Proceedings of the 10th SPIN Workshop on Model Checking Software. Lecture Notes in Computer Science","volume":"2648","author":"Henzinger T. A.","unstructured":"T. A. Henzinger , R. Jhala , R. Majumdar , and G. Sutre . 2003. Software verification with Blast . In Proceedings of the 10th SPIN Workshop on Model Checking Software. Lecture Notes in Computer Science , vol. 2648 , Springer, (Portland, OR). 235--239. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. 2003. Software verification with Blast. In Proceedings of the 10th SPIN Workshop on Model Checking Software. Lecture Notes in Computer Science, vol. 2648, Springer, (Portland, OR). 235--239."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1266840.1266854"},{"key":"e_1_2_1_67_1","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","unstructured":"C. A. R. Hoare . 1985. Communicating Sequential Processes . Prentice Hall . C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice Hall."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133572.1133615"},{"key":"e_1_2_1_69_1","volume-title":"Proceedings of the 2nd Workshop on Programming Languages and Operating Systems (PLOS).","author":"Hohmuth M.","unstructured":"M. Hohmuth and H. Tews . 2005. The VFiasco approach for a verified operating system . In Proceedings of the 2nd Workshop on Programming Languages and Operating Systems (PLOS). M. Hohmuth and H. Tews. 2005. The VFiasco approach for a verified operating system. In Proceedings of the 2nd Workshop on Programming Languages and Operating Systems (PLOS)."},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.10"},{"key":"e_1_2_1_71_1","first-page":"03","article-title":"U.S. government protection profile for separation kernels in environments requiring high robustness","volume":"1","author":"Directorate Information Assurance","year":"2007","unstructured":"Information Assurance Directorate . 2007 . U.S. government protection profile for separation kernels in environments requiring high robustness . Information Assurance Directorate, Version 1 . 03 . http:\/\/www. niap-ccevs.org\/cc-scheme\/pp\/pp.cfm\/id\/pp_skpp_hr_v1.03\/. Information Assurance Directorate. 2007. U.S. government protection profile for separation kernels in environments requiring high robustness. Information Assurance Directorate, Version 1.03. http:\/\/www. niap-ccevs.org\/cc-scheme\/pp\/pp.cfm\/id\/pp_skpp_hr_v1.03\/.","journal-title":"Information Assurance Directorate, Version"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0002-4"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596566"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_76_1","unstructured":"G. Klein T. Murray P. Gammie T. Sewell and S. Winwood. 2011. Provable security: How feasible is it&quest; In Proceedings of the 13th Workshop on Hot Topics in Operating Systems. (Napa CA). USENIX Association 28--32. G. Klein T. Murray P. Gammie T. Sewell and S. Winwood. 2011. Provable security: How feasible is it&quest; In Proceedings of the 13th Workshop on Hot Topics in Operating Systems. (Napa CA). USENIX Association 28--32."},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_20"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.23"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/1851276.1851284"},{"key":"e_1_2_1_82_1","unstructured":"L4HQ. 2007. http:\/\/l4hq.org\/arch\/arm\/. L4HQ. 2007. http:\/\/l4hq.org\/arch\/arm\/."},{"key":"e_1_2_1_83_1","unstructured":"L4Ka Team. 2004. L4Ka::Pistachio kernel. http:\/\/l4ka.org\/projects\/pistachio\/. L4Ka Team. 2004. L4Ka::Pistachio kernel. http:\/\/l4ka.org\/projects\/pistachio\/."},{"key":"e_1_2_1_84_1","volume-title":"Protection. In Proceedings of the 5th Princeton Symposium on Information Sciences and Systems","author":"Lampson B. W.","year":"1971","unstructured":"B. W. Lampson . 1971 . Protection. In Proceedings of the 5th Princeton Symposium on Information Sciences and Systems . Princeton University, 437--443. B. W. Lampson. 1971. Protection. In Proceedings of the 5th Princeton Symposium on Information Sciences and Systems. Princeton University, 437--443."},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_87_1","unstructured":"X. Leroy. 2012. Compcert version 1.10. http:\/\/compcert.inria.fr. X. Leroy. 2012. Compcert version 1.10. http:\/\/compcert.inria.fr."},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.014"},{"key":"e_1_2_1_89_1","volume-title":"Proceedings of the 16th IEEE Real-Time Systems Symposium. IEEE, 298--307","author":"Li Y.-T.","unstructured":"Y.-T. Li , S. Malik , and A. Wolfe . 1995. Efficient microarchitecture modeling and path analysis for real-time software . In Proceedings of the 16th IEEE Real-Time Systems Symposium. IEEE, 298--307 . Y.-T. Li, S. Malik, and A. Wolfe. 1995. Efficient microarchitecture modeling and path analysis for real-time software. In Proceedings of the 16th IEEE Real-Time Systems Symposium. IEEE, 298--307."},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168633"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/234215.234473"},{"key":"e_1_2_1_92_1","volume-title":"Proceedings of the 6th Workshop on Hot Topics in Operating Systems. 28--31","author":"Liedtke J.","unstructured":"J. Liedtke , K. Elphinstone , S. Sch\u00f6nberg , H. H\u00e4rtig , G. Heiser , N. Islam , and T. Jaeger . 1997. Achieved IPC performance (still the foundation for extensibility) . In Proceedings of the 6th Workshop on Hot Topics in Operating Systems. 28--31 . J. Liedtke, K. Elphinstone, S. Sch\u00f6nberg, H. H\u00e4rtig, G. Heiser, N. Islam, and T. Jaeger. 1997. Achieved IPC performance (still the foundation for extensibility). In Proceedings of the 6th Workshop on Hot Topics in Operating Systems. 28--31."},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/322017.322025"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSE.2009.82"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICESS.2009.24"},{"key":"e_1_2_1_96_1","volume-title":"Proceedings of the 15th IEEE\/ACM International Conference on Automated Software Engineering. IEEE, 133--141","author":"Martin W. B.","unstructured":"W. B. Martin , P. White , F. Taylor , and A. Goldberg . 2000. Formal construction of the mathematically analyzed separation kernel . In Proceedings of the 15th IEEE\/ACM International Conference on Automated Software Engineering. IEEE, 133--141 . W. B. Martin, P. White, F. Taylor, and A. Goldberg. 2000. Formal construction of the mathematically analyzed separation kernel. In Proceedings of the 15th IEEE\/ACM International Conference on Automated Software Engineering. IEEE, 133--141."},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016324624000"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_23"},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_12"},{"key":"e_1_2_1_102_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792248"},{"key":"e_1_2_1_103_1","unstructured":"NICTA. 2006. Iguana. http:\/\/www.ertos.nicta.com.au\/software\/kenge\/iguana-project\/latest\/. NICTA. 2006. Iguana. http:\/\/www.ertos.nicta.com.au\/software\/kenge\/iguana-project\/latest\/."},{"key":"e_1_2_1_104_1","unstructured":"NICTA. 2013a. sel4 microkernel. http:\/\/ertos.nicta.com.au\/research\/sel4\/. NICTA. 2013a. sel4 microkernel. http:\/\/ertos.nicta.com.au\/research\/sel4\/."},{"key":"e_1_2_1_105_1","unstructured":"NICTA. 2013b. Worst-case execution time computation tools. http:\/\/ssrg.nicta.com.au\/software\/TS\/wcet- tools\/. NICTA. 2013b. Worst-case execution time computation tools. http:\/\/ssrg.nicta.com.au\/software\/TS\/wcet- tools\/."},{"key":"e_1_2_1_106_1","volume-title":"Lecture Notes in Computer Science","volume":"2283","author":"Nipkow T.","unstructured":"T. Nipkow , L. Paulson , and M. Wenzel . 2002. Isabelle\/HOL \u2014 A proof assistant for higher-order logic . In Lecture Notes in Computer Science , vol. 2283 , Springer. T. Nipkow, L. Paulson, and M. Wenzel. 2002. Isabelle\/HOL \u2014 A proof assistant for higher-order logic. In Lecture Notes in Computer Science, vol. 2283, Springer."},{"key":"e_1_2_1_107_1","unstructured":"Open Kernel Labs. 2008. OKL4 web site. http:\/\/wiki.ok-labs.com\/PreviousReleases. Open Kernel Labs. 2008. OKL4 web site. http:\/\/wiki.ok-labs.com\/PreviousReleases."},{"key":"e_1_2_1_108_1","volume-title":"Proceedings of the NSAS Formal Methods Symposium. Springer, 298--312","author":"Peleska J.","unstructured":"J. Peleska , E. Vorobev , and F. Lapschies . 2011. Automated test case generation with SMT-solving and abstract interpretation . In Proceedings of the NSAS Formal Methods Symposium. Springer, 298--312 . J. Peleska, E. Vorobev, and F. Lapschies. 2011. Automated test case generation with SMT-solving and abstract interpretation. In Proceedings of the NSAS Formal Methods Symposium. Springer, 298--312."},{"key":"e_1_2_1_109_1","volume-title":"Proceedings of the DoD\/NBS Computer Security Initiative Conference. 146--160","author":"Perrine T.","unstructured":"T. Perrine , J. Codd , and B. Hardy . 1984. An overview of the kernelized secure operating system (KSOS) . In Proceedings of the DoD\/NBS Computer Security Initiative Conference. 146--160 . T. Perrine, J. Codd, and B. Hardy. 1984. An overview of the kernelized secure operating system (KSOS). In Proceedings of the DoD\/NBS Computer Security Initiative Conference. 146--160."},{"key":"e_1_2_1_110_1","unstructured":"QNX. 2012. Operating systems. http:\/\/www.qnx.com\/products\/neutrino-rtos\/. QNX. 2012. Operating systems. http:\/\/www.qnx.com\/products\/neutrino-rtos\/."},{"key":"e_1_2_1_111_1","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"Richards R. J.","unstructured":"R. J. Richards . 2010. Modeling and security analysis of a commercial real-time operating system kernel . In Design and Verification of Microprocessor Systems for High-Assurance Applications , D. S. Hardin, Ed., Springer , 301--322. R. J. Richards. 2010. Modeling and security analysis of a commercial real-time operating system kernel. In Design and Verification of Microprocessor Systems for High-Assurance Applications, D. S. Hardin, Ed., Springer, 301--322."},{"key":"e_1_2_1_113_1","doi-asserted-by":"publisher","DOI":"10.1145\/800216.806586"},{"key":"e_1_2_1_114_1","doi-asserted-by":"publisher","DOI":"10.1007\/11925040_10"},{"key":"e_1_2_1_115_1","volume-title":"Proceedings of the National Computer Security Conference. 129--141","author":"Saydjari O.","unstructured":"O. Saydjari , J. Beckman , and J. Leaman . 1987. LOCKing computers securely . In Proceedings of the National Computer Security Conference. 129--141 . O. Saydjari, J. Beckman, and J. Leaman. 1987. LOCKing computers securely. In Proceedings of the National Computer Security Conference. 129--141."},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294294"},{"key":"e_1_2_1_117_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_2_1_118_1","doi-asserted-by":"crossref","unstructured":"T. Sewell S. Winwood P. Gammie T. Murray J. Andronick and G. Klein . 2011 . seL4 enforces integrity. In Proceedings of the 2nd International Conference on Interactive Theorem Proving. M. C. J. D. van Eekelen H. Geuvers J. Schmaltz and F. Wiedijk Eds. Lecture Notes in Computer Science vol. 6898 Springer (The Netherlands). 325--340. T. Sewell S. Winwood P. Gammie T. Murray J. Andronick and G. Klein. 2011. seL4 enforces integrity. In Proceedings of the 2nd International Conference on Interactive Theorem Proving. M. C. J. D. van Eekelen H. Geuvers J. Schmaltz and F. Wiedijk Eds. Lecture Notes in Computer Science vol. 6898 Springer (The Netherlands). 325--340.","DOI":"10.1007\/978-3-642-22863-6_24"},{"key":"e_1_2_1_119_1","volume-title":"Proceedings of the 5th IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS). IEEE, 89--100","author":"Shapiro J. S.","unstructured":"J. S. Shapiro , D. F. Faber , and J. M. Smith . 1996. State caching in the EROS kernel\u2014implementing efficient orthogonal peristence in a pure capability system . In Proceedings of the 5th IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS). IEEE, 89--100 . J. S. Shapiro, D. F. Faber, and J. M. Smith. 1996. State caching in the EROS kernel\u2014implementing efficient orthogonal peristence in a pure capability system. In Proceedings of the 5th IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS). IEEE, 89--100."},{"key":"e_1_2_1_120_1","doi-asserted-by":"publisher","DOI":"10.1145\/319151.319163"},{"key":"e_1_2_1_121_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy. IEEE, 166--181","author":"Shapiro J. S.","unstructured":"J. S. Shapiro and S. Weber . 2000. Verifying the EROS confinement mechanism . In Proceedings of the IEEE Symposium on Security and Privacy. IEEE, 166--181 . J. S. Shapiro and S. Weber. 2000. Verifying the EROS confinement mechanism. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE, 166--181."},{"key":"e_1_2_1_122_1","volume-title":"Proceedings of the 1st International Workshop on Microkernels for Embedded Systems (MIKES). NICTA.","author":"Singal M.","unstructured":"M. Singal and S. M. Petters . 2007. Issues in analysing L4 for its WCET . In Proceedings of the 1st International Workshop on Microkernels for Embedded Systems (MIKES). NICTA. M. Singal and S. M. Petters. 2007. Issues in analysing L4 for its WCET. In Proceedings of the 1st International Workshop on Microkernels for Embedded Systems (MIKES). NICTA."},{"key":"e_1_2_1_123_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217951"},{"key":"e_1_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_2_1_125_1","volume-title":"Proceedings of the 8th USENIX Security Symposium. USENIX Association. 123--139","author":"Spencer R.","unstructured":"R. Spencer , S. Smalley , P. Loscocco , M. Hibler , D. Andersen , and J. Lepreau . 1999. The Flask security architecture: System support for diverse security policies . In Proceedings of the 8th USENIX Security Symposium. USENIX Association. 123--139 . R. Spencer, S. Smalley, P. Loscocco, M. Hibler, D. Andersen, and J. Lepreau. 1999. The Flask security architecture: System support for diverse security policies. In Proceedings of the 8th USENIX Security Symposium. USENIX Association. 123--139."},{"key":"e_1_2_1_126_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755913.1755935"},{"key":"e_1_2_1_127_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.043"},{"key":"e_1_2_1_129_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9120-2"},{"key":"e_1_2_1_130_1","unstructured":"H. Tuch G. Klein and G. Heiser. 2005. OS verification\u2014now&excl; In Proceedings of the 10th Workshop on Hot Topics in Operating Systems. 7--12. H. Tuch G. Klein and G. Heiser. 2005. OS verification\u2014now&excl; In Proceedings of the 10th Workshop on Hot Topics in Operating Systems. 7--12."},{"key":"e_1_2_1_131_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_2_1_132_1","series-title":"Lecture Notes in Computer Science","volume-title":"Information flow control revisited: Noninfluence = noninterference &plus","author":"von Oheimb D.","unstructured":"D. von Oheimb . 2004. Information flow control revisited: Noninfluence = noninterference &plus ; nonleakage. In Proceedings of the 9th European Symposium on Research in Computer Security. P. Samarati, P. Ryan, D. Gollmann, and R. Molva, Eds., Lecture Notes in Computer Science , vol. 3193 , Springer , 225--243. D. von Oheimb. 2004. Information flow control revisited: Noninfluence = noninterference &plus; nonleakage. In Proceedings of the 9th European Symposium on Research in Computer Security. P. Samarati, P. Ryan, D. Gollmann, and R. Molva, Eds., Lecture Notes in Computer Science, vol. 3193, Springer, 225--243."},{"key":"e_1_2_1_133_1","volume-title":"Proceedings of the 6th International Verification Workshop. M. Aderhold, S. Autexier, and H. Mantel, Eds., EasyChair Proceedings in Computing","volume":"3","author":"von Tessin M.","year":"2010","unstructured":"M. von Tessin . 2010 . Towards high-assurance multiprocessor virtualisation . In Proceedings of the 6th International Verification Workshop. M. Aderhold, S. Autexier, and H. Mantel, Eds., EasyChair Proceedings in Computing , vol. 3 , EasyChair, 110--125. M. von Tessin. 2010. Towards high-assurance multiprocessor virtualisation. In Proceedings of the 6th International Verification Workshop. M. Aderhold, S. Autexier, and H. Mantel, Eds., EasyChair Proceedings in Computing, vol. 3, EasyChair, 110--125."},{"key":"e_1_2_1_134_1","volume-title":"Proceedings of the 2nd Workshop on Systems for Future Multi-Core Architectures. Microsoft, 1--6.","author":"von Tessin M.","year":"2012","unstructured":"M. von Tessin . 2012 . The clustered multikernel: An approach to formal verification of multiprocessor OS kernels . In Proceedings of the 2nd Workshop on Systems for Future Multi-Core Architectures. Microsoft, 1--6. M. von Tessin. 2012. The clustered multikernel: An approach to formal verification of multiprocessor OS kernels. In Proceedings of the 2nd Workshop on Systems for Future Multi-Core Architectures. Microsoft, 1--6."},{"key":"e_1_2_1_136_1","doi-asserted-by":"publisher","DOI":"10.1145\/358818.358825"},{"key":"e_1_2_1_137_1","unstructured":"D. A. Wheeler. 2001. SLOCCount. http:\/\/www.dwheeler.com\/sloccount\/. D. A. Wheeler. 2001. SLOCCount. http:\/\/www.dwheeler.com\/sloccount\/."},{"key":"e_1_2_1_138_1","doi-asserted-by":"publisher","DOI":"10.5555\/1060289.1060308"},{"key":"e_1_2_1_139_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_2_1_140_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_34"},{"key":"e_1_2_1_141_1","doi-asserted-by":"publisher","DOI":"10.1145\/355616.364017"},{"key":"e_1_2_1_142_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"e_1_2_1_143_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018396.2018419"}],"container-title":["ACM Transactions on Computer Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2560537","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2560537","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:21Z","timestamp":1750219821000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2560537"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":134,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.1145\/2560537"],"URL":"https:\/\/doi.org\/10.1145\/2560537","relation":{},"ISSN":["0734-2071","1557-7333"],"issn-type":[{"value":"0734-2071","type":"print"},{"value":"1557-7333","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2]]},"assertion":[{"value":"2013-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-02-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}