{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T03:14:25Z","timestamp":1776482065759,"version":"3.51.2"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"10","license":[{"start":{"date-parts":[[2018,9,26]],"date-time":"2018-09-26T00:00:00Z","timestamp":1537920000000},"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":[[2018,9,26]]},"abstract":"<jats:p>Verified software secures the Unmanned Little Bird autonomous helicopter against mid-flight cyber attacks.<\/jats:p>","DOI":"10.1145\/3230627","type":"journal-article","created":{"date-parts":[[2018,9,26]],"date-time":"2018-09-26T16:25:19Z","timestamp":1537979119000},"page":"68-77","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Formally verified software in the real world"],"prefix":"10.1145","volume":"61","author":[{"given":"Gerwin","family":"Klein","sequence":"first","affiliation":[{"name":"Data61, CSIRO and UNSW, Sydney, Australia"}]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[{"name":"Data61, CSIRO and UNSW, Sydney, Australia"}]},{"given":"Matthew","family":"Fernandez","sequence":"additional","affiliation":[{"name":"UNSW, Sydney, Australia and Intel Labs"}]},{"given":"Ihor","family":"Kuz","sequence":"additional","affiliation":[{"name":"Data61, CSIRO and UNSW, Sydney, Australia"}]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[{"name":"University of Melbourne, Australia and Data61, CSIRO"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"UNSW, Sydney, Australia and Data61, CSIRO"}]}],"member":"320","published-online":{"date-parts":[[2018,9,26]]},"reference":[{"key":"e_1_2_2_1_1","first-page":"3","article-title":"The MILS architecture for high-assurance embedded systems","volume":"2","author":"Alves-Foss J.","year":"2006","unstructured":"Alves-Foss , J. , Oman , P.W. , Taylor , C. , and Harrison , S . The MILS architecture for high-assurance embedded systems . International Journal of Embedded Systems 2 , 3 -- 4 ( 2006 ), 239--247. Alves-Foss, J., Oman, P.W., Taylor, C., and Harrison, S. The MILS architecture for high-assurance embedded systems. International Journal of Embedded Systems 2, 3--4 (2006), 239--247.","journal-title":"International Journal of Embedded Systems"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"e_1_2_2_3_1","unstructured":"Boeing. Unmanned Little Bird H-6U; http:\/\/www.boeing.com\/defense\/unmanned-little-bird-h-6u\/  Boeing. Unmanned Little Bird H-6U; http:\/\/www.boeing.com\/defense\/unmanned-little-bird-h-6u\/"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the 15<sup>th<\/sup> International Conference on Formal Engineering Methods (Queenstown, New Zealand, Oct. 29-Nov. 1)","author":"Boyton A.","year":"2013","unstructured":"Boyton , A. , Andronick , J. , Bannister , C. , Fernandez , M. , Gao , X. , Greenaway , D. , Klein , G. , Lewis , C. , and Sewell , T . Formally verified system initialisation . In Proceedings of the 15<sup>th<\/sup> International Conference on Formal Engineering Methods (Queenstown, New Zealand, Oct. 29-Nov. 1) . Springer , Heidelberg, Germany , 2013 70--85. Boyton, A., Andronick, J., Bannister, C., Fernandez, M., Gao, X., Greenaway, D., Klein, G., Lewis, C., and Sewell, T. Formally verified system initialisation. In Proceedings of the 15<sup>th<\/sup> International Conference on Formal Engineering Methods (Queenstown, New Zealand, Oct. 29-Nov. 1). Springer, Heidelberg, Germany, 2013 70--85."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660294"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"e_1_2_2_8_1","volume-title":"Proceedings of the International Society of Parametric Analysts \/ Society of Cost Estimating and Analysis 2008 Joint International Conference (Noordwijk, the Netherlands, May 12--14)","author":"Colbert E.","year":"2008","unstructured":"Colbert , E. and Boehm , B . Cost estimation for secure software & systems . In Proceedings of the International Society of Parametric Analysts \/ Society of Cost Estimating and Analysis 2008 Joint International Conference (Noordwijk, the Netherlands, May 12--14) . Curran, Red Hook, NY , 2008 . Colbert, E. and Boehm, B. Cost estimation for secure software & systems. In Proceedings of the International Society of Parametric Analysts \/ Society of Cost Estimating and Analysis 2008 Joint International Conference (Noordwijk, the Netherlands, May 12--14). Curran, Red Hook, NY, 2008."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9324-6"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804318"},{"key":"e_1_2_2_13_1","volume-title":"Proceedings of the 20<sup>th<\/sup> International Symposium on Formal Methods (Oslo, Norway, June 22--26)","author":"Fernandez M.","year":"2015","unstructured":"Fernandez , M. , Andronick , J. , Klein , G. , and Kuz , I . Automated verification of RPC stub code . In Proceedings of the 20<sup>th<\/sup> International Symposium on Formal Methods (Oslo, Norway, June 22--26) . Springer , Heidelberg, Germany , 2015 , 273--290. Fernandez, M., Andronick, J., Klein, G., and Kuz, I. Automated verification of RPC stub code. In Proceedings of the 20<sup>th<\/sup> International Symposium on Formal Methods (Oslo, Norway, June 22--26). Springer, Heidelberg, Germany, 2015, 273--290."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_2_15_1","volume-title":"A Computer-Checked Proof of the Four-Colour Theorem. Microsoft Research","author":"Gonthier G.","year":"2005","unstructured":"Gonthier , G. A Computer-Checked Proof of the Four-Colour Theorem. Microsoft Research , Cambridge , U.K , 2005 ; https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/gonthier-4colproof.pdf Gonthier, G. A Computer-Checked Proof of the Four-Colour Theorem. Microsoft Research, Cambridge, U.K, 2005; https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/gonthier-4colproof.pdf"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_2_2_17_1","volume-title":"Proceedings of the 12<sup>th<\/sup> USENIX Symposium on Operating Systems Design and Implementation (Savannah, GA, Nov. 2--4)","author":"Gu R.","year":"2016","unstructured":"Gu , R. , Shao , Z. , Chen , H. , Wu , X. (N.)., Kim , J. , Sj\u00f6berg , V. , and Costanzo , C . CertiKOS: An extensible architecture for building certified concurrent OS kernels . In Proceedings of the 12<sup>th<\/sup> USENIX Symposium on Operating Systems Design and Implementation (Savannah, GA, Nov. 2--4) . ACM Press , New York , 2016 . Gu, R., Shao, Z., Chen, H., Wu, X.(N.)., Kim, J., Sj\u00f6berg, V., and Costanzo, C. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the 12<sup>th<\/sup> USENIX Symposium on Operating Systems Design and Implementation (Savannah, GA, Nov. 2--4). ACM Press, New York, 2016."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2893177"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_11"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9357-x"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1851276.1851284"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2006.08.039"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_2_2_30_1","volume-title":"Proceedings of the Fourth International Conference on Tools and Algorithms for Construction and Analysis of Systems (Lisbon, Portugal, Mar. 28-Apr. 4)","author":"Pnueli A.","year":"1998","unstructured":"Pnueli , A. , Siegel , M. , and Singerman , E . Translation validation . In Proceedings of the Fourth International Conference on Tools and Algorithms for Construction and Analysis of Systems (Lisbon, Portugal, Mar. 28-Apr. 4) . Springer, Berlin , Germany , 1998 , 151--166. Pnueli, A., Siegel, M., and Singerman, E. Translation validation. In Proceedings of the Fourth International Conference on Tools and Algorithms for Construction and Analysis of Systems (Lisbon, Portugal, Mar. 28-Apr. 4). Springer, Berlin, Germany, 1998, 151--166."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/800216.806586"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629583"},{"key":"e_1_2_2_33_1","unstructured":"seL4 microkernel code and proofs; https:\/\/github.com\/seL4\/  seL4 microkernel code and proofs; https:\/\/github.com\/seL4\/"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2016.7461326"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2033939.2033965"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3230627","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3230627","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:39:47Z","timestamp":1750210787000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3230627"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,26]]},"references-count":35,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2018,9,26]]}},"alternative-id":["10.1145\/3230627"],"URL":"https:\/\/doi.org\/10.1145\/3230627","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9,26]]},"assertion":[{"value":"2018-09-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}