{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T03:30:27Z","timestamp":1792726227139,"version":"4.5.0"},"publisher-location":"New York, NY, USA","reference-count":64,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,10,4]],"date-time":"2015-10-04T00:00:00Z","timestamp":1443916800000},"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":[],"published-print":{"date-parts":[[2015,10,4]]},"DOI":"10.1145\/2815400.2815428","type":"proceedings-article","created":{"date-parts":[[2015,10,1]],"date-time":"2015-10-01T12:01:58Z","timestamp":1443700918000},"page":"1-17","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":263,"title":["IronFleet"],"prefix":"10.1145","author":[{"given":"Chris","family":"Hawblitzel","sequence":"first","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jon","family":"Howell","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Manos","family":"Kapritsos","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jacob R.","family":"Lorch","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael L.","family":"Roberts","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Srinath","family":"Setty","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brian","family":"Zill","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,10,4]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2011.5958208"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1243418.1243422"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1267308.1267332"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/571637.571640"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/859246.859249"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/646733.701301"},{"key":"e_1_3_2_2_10_1","volume-title":"Inc.","author":"Constable R. L.","year":"1986","unstructured":"Constable , R. L. , Allen , S. F. , Bromley , H. M. , Cleaveland , W. R. , Cremer , J. F. , Harper , R. W. , Howe , D. J. , Knoblock , T. B. , Mendler , N. P. , Panangaden , P. , Sasaki , J. T. , and Smith , S. F . Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall , Inc. , 1986 . Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki, J. T., and Smith, S. F. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., 1986."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1267308.1267331"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480885"},{"key":"e_1_3_2_2_15_1","volume-title":"https:\/\/github.com\/efficient\/epaxos\/","author":"Paxos","year":"2013","unstructured":"E Paxos code. https:\/\/github.com\/efficient\/epaxos\/ , 2013 . EPaxos code. https:\/\/github.com\/efficient\/epaxos\/, 2013."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_3_2_2_17_1","volume-title":"Proceedings of Symposia in Applied Mathematics","author":"Floyd R.","year":"1967","unstructured":"Floyd , R. Assigning meanings to programs . In Proceedings of Symposia in Applied Mathematics ( 1967 ). Floyd, R. Assigning meanings to programs. In Proceedings of Symposia in Applied Mathematics (1967)."},{"key":"e_1_3_2_2_18_1","first-page":"13","author":"Garland S. J.","year":"2000","unstructured":"Garland , S. J. , and Lynch , N. A. Using I\/O automata for developing distributed systems. Foundations of Component-Based Systems 13 ( 2000 ). Garland, S. J., and Lynch, N. A. Using I\/O automata for developing distributed systems. Foundations of Component-Based Systems 13 (2000).","journal-title":"Foundations of Component-Based Systems"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043582"},{"key":"e_1_3_2_2_21_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (October","author":"Hawblitzel C.","year":"2014","unstructured":"Hawblitzel , C. , Howell , J. , Lorch , J. R. , Narayan , A. , Parno , B. , Zhang , D. , and Zill , B . Ironclad apps: End-to-end security via automated full-system verification . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (October 2014 ). Hawblitzel, C., Howell, J., Lorch, J. R., Narayan, A., Parno, B., Zhang, D., and Zill, B. Ironclad apps: End-to-end security via automated full-system verification. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (October 2014)."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_2_24_1","volume-title":"Proceedings of the USENIX Annual Technical Conference (ATC)","author":"Hunt P.","year":"2010","unstructured":"Hunt , P. , Konar , M. , Junqueira , F. P. , and Reed , B . ZooKeeper: Wait-free coordination for Internet-scale systems . In Proceedings of the USENIX Annual Technical Conference (ATC) ( 2010 ). Hunt, P., Konar, M., Junqueira, F. P., and Reed, B. ZooKeeper: Wait-free coordination for Internet-scale systems. In Proceedings of the USENIX Annual Technical Conference (ATC) (2010)."},{"key":"e_1_3_2_2_25_1","volume-title":"https:\/\/research.microsoft.com\/projects\/ironclad\/","author":"IronFleet","year":"2015","unstructured":"IronFleet code. https:\/\/research.microsoft.com\/projects\/ironclad\/ , 2015 . IronFleet code. https:\/\/research.microsoft.com\/projects\/ironclad\/, 2015."},{"key":"e_1_3_2_2_26_1","unstructured":"Jones E. Model checking a Paxos implementation. http:\/\/www.evanjones.ca\/model-checking-paxos.html 2009.  Jones E. Model checking a Paxos implementation. http:\/\/www.evanjones.ca\/model-checking-paxos.html 2009."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022969405325"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2011.5958223"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250755"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_2_36_1","volume-title":"Specifying Systems: The TLA+ Languange and Tools for Hardware and Software Engineers","author":"Lamport L.","year":"2002","unstructured":"Lamport , L. Specifying Systems: The TLA+ Languange and Tools for Hardware and Software Engineers . Addison-Wesley , 2002 . Lamport, L. Specifying Systems: The TLA+ Languange and Tools for Hardware and Software Engineers. Addison-Wesley, 2002."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03466-4_2"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/2075029.2075058"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217946"},{"key":"e_1_3_2_2_42_1","volume-title":"Workshop on Automated Verification of Critical Systems","author":"Lu T.","year":"2010","unstructured":"Lu , T. , Merz , S. , Weidenbach , C. , Bendisposto , J. , Leuschel , M. , Roggenbach , M. , Margaria , T. , Padberg , J. , Taentzer , G. , Lu , T. , Merz , S. , and Weidenbach , C . Model checking the Pastry routing protocol . In Workshop on Automated Verification of Critical Systems ( 2010 ). Lu, T., Merz, S., Weidenbach, C., Bendisposto, J., Leuschel, M., Roggenbach, M., Margaria, T., Padberg, J., Taentzer, G., Lu, T., Merz, S., and Weidenbach, C. Model checking the Pastry routing protocol. In Workshop on Automated Verification of Critical Systems (2010)."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451148"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2517350"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/1060289.1060297"},{"key":"e_1_3_2_2_47_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Musuvathi M.","year":"2008","unstructured":"Musuvathi , M. , Qadeer , S. , Ball , T. , Basler , G. , Nainar , P. A. , and Neamtiu , I . Finding and reproducing heisenbugs in concurrent programs . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) ( 2008 ). Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P. A., and Neamtiu, I. Finding and reproducing heisenbugs in concurrent programs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (2008)."},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_2_2_50_1","volume-title":"Proceedings of the USENIX Annual Technical Conference (ATC) (June","author":"Ongaro D.","year":"2014","unstructured":"Ongaro , D. , and Ousterhour , J . In search of an understandable consensus algorithm . In Proceedings of the USENIX Annual Technical Conference (ATC) (June 2014 ). Ongaro, D., and Ousterhour, J. In search of an understandable consensus algorithm. In Proceedings of the USENIX Annual Technical Conference (ATC) (June 2014)."},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/1884866.1884885"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.38"},{"key":"e_1_3_2_2_53_1","volume-title":"Proceedings of the Joint Conferences on Computers in Technical Systems and Intelligent Systems","author":"Pek E.","year":"2003","unstructured":"Pek , E. , and Bogunovic , N . Formal verification of communication protocols in distributed systems . In Proceedings of the Joint Conferences on Computers in Technical Systems and Intelligent Systems ( 2003 ). Pek, E., and Bogunovic, N. Formal verification of communication protocols in distributed systems. In Proceedings of the Joint Conferences on Computers in Technical Systems and Intelligent Systems (2003)."},{"key":"e_1_3_2_2_54_1","volume-title":"Papers on Time and Tense","author":"Prior A. N.","year":"1968","unstructured":"Prior , A. N. Papers on Time and Tense . Oxford University Press , 1968 . Prior, A. N. Papers on Time and Tense. Oxford University Press, 1968."},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/645954.675657"},{"key":"e_1_3_2_2_56_1","volume-title":"Proceedings of the International Workshop on User Interfaces for Theorem Provers (UITP) (July","author":"Rahli V.","year":"2012","unstructured":"Rahli , V. Interfacing with proof assistants for domain specific programming using EventML . In Proceedings of the International Workshop on User Interfaces for Theorem Provers (UITP) (July 2012 ). Rahli, V. Interfacing with proof assistants for domain specific programming using EventML. In Proceedings of the International Workshop on User Interfaces for Theorem Provers (UITP) (July 2012)."},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2014.45"},{"key":"e_1_3_2_2_58_1","volume-title":"http:\/\/redis.io\/. Implementation used: version 2.8.2101 of the MSOpenTech distribution https:\/\/github.com\/MSOpenTech\/redis","author":"Redis","year":"2015","unstructured":"Redis . http:\/\/redis.io\/. Implementation used: version 2.8.2101 of the MSOpenTech distribution https:\/\/github.com\/MSOpenTech\/redis , 2015 . Redis. http:\/\/redis.io\/. Implementation used: version 2.8.2101 of the MSOpenTech distribution https:\/\/github.com\/MSOpenTech\/redis, 2015."},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480934"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/SRDS.2013.22"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/ITI.2001.938054"},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/383059.383071"},{"key":"e_1_3_2_2_63_1","volume-title":"MIT Laboratory for Computer Science","author":"Stoica I.","year":"2001","unstructured":"Stoica , I. , Morris , R. , Karger , D. , Kaashoek , M. F. , and Balakrishnan , H . Chord: A scalable peer-to-peer lookup service for Internet applications. Tech. Rep. MIT\/LCS\/TR-819 , MIT Laboratory for Computer Science , March 2001 . Stoica, I., Morris, R., Karger, D., Kaashoek, M. F., and Balakrishnan, H. Chord: A scalable peer-to-peer lookup service for Internet applications. Tech. Rep. MIT\/LCS\/TR-819, MIT Laboratory for Computer Science, March 2001."},{"key":"e_1_3_2_2_64_1","volume-title":"International Workshop on Microprocessor Test and Verification (June","author":"Tasiran S.","year":"2002","unstructured":"Tasiran , S. , Yu , Y. , Batson , B. , and Kreider , S . Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor . In International Workshop on Microprocessor Test and Verification (June 2002 ), IEEE. Tasiran, S., Yu, Y., Batson, B., and Kreider, S. Using formal specifications to monitor and guide simulation: Verifying the cache coherence engine of the Alpha 21364 microprocessor. In International Workshop on Microprocessor Test and Verification (June 2002), IEEE."},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.1599419"},{"key":"e_1_3_2_2_66_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (December","author":"Wang Y.","year":"2008","unstructured":"Wang , Y. , Kelly , T. , Kudlur , M. , Lafortune , S. , and Mahlke , S. A . Gadara: Dynamic deadlock avoidance for multithreaded programs . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (December 2008 ). Wang, Y., Kelly, T., Kudlur, M., Lafortune, S., and Mahlke, S. A. Gadara: Dynamic deadlock avoidance for multithreaded programs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (December 2008)."},{"key":"e_1_3_2_2_67_1","volume-title":"August","author":"Wilcox J.","year":"2015","unstructured":"Wilcox , J. , Woos , D. , Panchekha , P. , Tatlock , Z. , Wang , X. , Ernst , M. , and Anderson , T . UW CSE News: UW CSE's Verdi team completes first full formal verification of Raft consensus protocol. https:\/\/news.cs.washington.edu\/2015\/08\/07\/ , August 2015 . Wilcox, J., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M., and Anderson, T. UW CSE News: UW CSE's Verdi team completes first full formal verification of Raft consensus protocol. https:\/\/news.cs.washington.edu\/2015\/08\/07\/, August 2015."},{"key":"e_1_3_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_2_69_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI) (April","author":"Yang J.","year":"2009","unstructured":"Yang , J. , Chen , T. , Wu , M. , Xu , Z. , Liu , X. , Lin , H. , Yang , M. , Long , F. , Zhang , L. , and Zhou , L . MODIST: Transparent model checking of unmodified distributed systems . In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI) (April 2009 ). Yang, J., Chen, T., Wu, M., Xu, Z., Liu, X., Lin, H., Yang, M., Long, F., Zhang, L., and Zhou, L. MODIST: Transparent model checking of unmodified distributed systems. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI) (April 2009)."},{"key":"e_1_3_2_2_70_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (October","author":"Yuan D.","year":"2014","unstructured":"Yuan , D. , Luo , Y. , Zhuang , X. , Rodrigues , G. R. , Zhao , X. , Zhang , Y. , Jain , P. U. , and Stumm , M . Simple testing can prevent most critical failures: An analysis of production failures in distributed data-intensive systems . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (October 2014 ). Yuan, D., Luo, Y., Zhuang, X., Rodrigues, G. R., Zhao, X., Zhang, Y., Jain, P. U., and Stumm, M. Simple testing can prevent most critical failures: An analysis of production failures in distributed data-intensive systems. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (October 2014)."},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185376.2185383"}],"event":{"name":"SOSP '15: ACM SIGOPS 25th Symposium on Operating Systems Principles","location":"Monterey California","acronym":"SOSP '15","sponsor":["SSRC Storage Systems Research Center, UC Santa Cruz","SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the 25th Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2815400.2815428","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2815400.2815428","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:43:13Z","timestamp":1750225393000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2815400.2815428"}},"subtitle":["proving practical distributed systems correct"],"short-title":[],"issued":{"date-parts":[[2015,10,4]]},"references-count":64,"alternative-id":["10.1145\/2815400.2815428","10.1145\/2815400"],"URL":"https:\/\/doi.org\/10.1145\/2815400.2815428","relation":{},"subject":[],"published":{"date-parts":[[2015,10,4]]},"assertion":[{"value":"2015-10-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}