{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T05:02:29Z","timestamp":1767934949561,"version":"3.49.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031606977","type":"print"},{"value":"9783031606984","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-60698-4_6","type":"book-chapter","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:01:51Z","timestamp":1716768111000},"page":"99-117","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying a\u00a0C Implementation of\u00a0Derecho\u2019s Coordination Mechanism Using VST and\u00a0Coq"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2779-2071","authenticated-orcid":false,"given":"Ramana","family":"Nagasamudram","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1570-3492","authenticated-orcid":false,"given":"Lennart","family":"Beringer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2400-149X","authenticated-orcid":false,"given":"Ken","family":"Birman","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3126-7771","authenticated-orcid":false,"given":"Mae","family":"Milano","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7634-6150","authenticated-orcid":false,"given":"David A.","family":"Naumann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,5,26]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Arntzenius, M., Krishnaswami, N.: Semina\u00efve evaluation for a higher-order functional language. Proc. ACM Program. Lang. 4(POPL), 22:1\u201322:28 (2020). https:\/\/doi.org\/10.1145\/3371090","DOI":"10.1145\/3371090"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1016\/j.scico.2017.08.003","volume":"158","author":"N Azmy","year":"2018","unstructured":"Azmy, N., Merz, S., Weidenbach, C.: A machine-checked correctness proof for Pastry. Sci. Comput. Program. 158, 64\u201380 (2018)","journal-title":"Sci. Comput. Program."},{"key":"6_CR3","unstructured":"Bieniusa, A., Haas, J., Kleppmann, M., Mogk, R. (eds.): Programming Local-First Software (ECOOP Workshop). European Conference on Object-Oriented Programming (2022). https:\/\/2022.ecoop.org\/home\/plf-2022"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-031-44274-2_14","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"K Birman","year":"2023","unstructured":"Birman, K., Jha, S., Milano, M., Rosa, L., Song, W., Tremel, E.: Monotonicity and opportunistically-batched actions in Derecho. In: Dolev, S., Schieber, B. (eds.) SSS 2023. LNCS, vol. 14310, pp. 172\u2013190. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44274-2_14"},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9457-5","volume":"61","author":"Q Cao","year":"2018","unstructured":"Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61, 367\u2013422 (2018)","journal-title":"J. Autom. Reason."},{"key":"6_CR6","unstructured":"Chajed, T., Tassarotti, J., Theng, M., Kaashoek, M.F., Zeldovich, N.: Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning. In: OSDI (2022)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Chand, S., Liu, Y.A., Stoller, S.D.: Formal verification of Multi-paxos for distributed consensus. ArXiv abs\/1606.01387 (2016)","DOI":"10.1007\/978-3-319-48989-6_8"},{"key":"6_CR8","unstructured":"Cheung, A., Crooks, N., Hellerstein, J.M., Milano, M.: New directions in cloud programming. In: Conference on Innovative Data Systems Research (CIDR) (2021). http:\/\/cidrdb.org\/cidr2021\/papers\/cidr2021_paper16.pdf"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Erbsen, A., Gruetter, S., Choi, J., Wood, C., Chlipala, A.: Integration verification across software and hardware for a simple embedded system. In: PLDI (2021)","DOI":"10.1145\/3410295"},{"key":"6_CR10","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning About Knowledge","author":"R Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Greenaway, D., Lim, J., Andronick, J., Klein, G.: Don\u2019t sweat the small stuff: formal verification of C code without the pain. In: PLDI (2014)","DOI":"10.1145\/2594291.2594296"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Grun, P., et al.: A brief introduction to the OpenFabrics interfaces - a new network API for maximizing high performance application efficiency. In: IEEE Annual Symposium on High-Performance Interconnects, pp. 34\u201339 (2015). https:\/\/doi.org\/10.1109\/HOTI.2015.19","DOI":"10.1109\/HOTI.2015.19"},{"issue":"7","key":"6_CR13","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/3068608","volume":"60","author":"C Hawblitzel","year":"2017","unstructured":"Hawblitzel, C., et al.: IronFleet: proving safety and liveness of practical distributed systems. Commun. ACM 60(7), 83\u201392 (2017)","journal-title":"Commun. ACM"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1145\/3369736","volume":"63","author":"JM Hellerstein","year":"2020","unstructured":"Hellerstein, J.M., Alvaro, P.: Keeping CALM: when distributed consistency is easy. Commun. ACM 63, 72\u201381 (2020)","journal-title":"Commun. ACM"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Honor\u00e9, W., Kim, J., Shin, J., Shao, Z.: Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201331 (2021). https:\/\/doi.org\/10.1145\/3485474","DOI":"10.1145\/3485474"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Honor\u00e9, W., Shin, J., Kim, J., Shao, Z.: Adore: atomic distributed objects with certified reconfiguration. In: Jhala, R., Dillig, I. (eds.) PLDI (2022)","DOI":"10.1145\/3519939.3523444"},{"key":"6_CR17","first-page":"1","volume":"36","author":"S Jha","year":"2019","unstructured":"Jha, S., et al.: Derecho: fast state machine replication for cloud services. ACM Trans. Comput. Syst. 36, 1\u201349 (2019)","journal-title":"ACM Trans. Comput. Syst."},{"key":"6_CR18","doi-asserted-by":"publisher","first-page":"e20","DOI":"10.1017\/S0956796818000151","volume":"28","author":"R Jung","year":"2018","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018)","journal-title":"J. Funct. Program."},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-030-44914-8_13","volume-title":"Programming Languages and Systems","author":"M Krogh-Jespersen","year":"2020","unstructured":"Krogh-Jespersen, M., Timany, A., Ohlenbusch, M.E., Gregersen, S.O., Birkedal, L.: Aneris: a mechanised logic for modular reasoning about distributed systems. In: ESOP 2020. LNCS, vol. 12075, pp. 336\u2013365. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_13"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Kuper, L., Turon, A., Krishnaswami, N.R., Newton, R.R.: Freeze after writing: quasi-deterministic parallel programming with LVars. In: POPL, pp. 257\u2013270 (2014). https:\/\/doi.org\/10.1145\/2535838.2535842","DOI":"10.1145\/2535838.2535842"},{"issue":"4","key":"6_CR21","doi-asserted-by":"publisher","first-page":"856","DOI":"10.14778\/3574245.3574268","volume":"16","author":"S Laddad","year":"2022","unstructured":"Laddad, S., Power, C., Milano, M., Cheung, A., Crooks, N., Hellerstein, J.M.: Keep CALM and CRDT on. Proc. VLDB Endow. 16(4), 856\u2013863 (2022). https:\/\/doi.org\/10.14778\/3574245.3574268","journal-title":"Proc. VLDB Endow."},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Laddad, S., Power, C., Milano, M., Cheung, A., Hellerstein, J.M.: Katara: Synthesizing CRDTs with verified lifting. Proc. ACM Program. Lang. 6(OOPSLA2), 1349\u20131377 (2022). https:\/\/doi.org\/10.1145\/3563336","DOI":"10.1145\/3563336"},{"issue":"7","key":"6_CR23","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107\u2013115 (2009)","journal-title":"CACM"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Mansky, W., Appel, A.W., Nogin, A.: A verified messaging system. In: OOPSLA (2017)","DOI":"10.1145\/3133911"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Mansky, W., Du, K.: An Iris instance for verifying CompCert C programs. Proc. ACM Program. Lang. 8(POPL), 148\u2013174 (2024)","DOI":"10.1145\/3632848"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Mansky, W., Honor\u00e9, W., Appel, A.W.: Connecting higher-order separation logic to a first-order outside world. In: ESOP (2020)","DOI":"10.26226\/morressier.604907f41a80aac83ca25d4c"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-030-53291-8_12","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2020","unstructured":"McMillan, K.L., Padon, O.: Ivy: a multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 190\u2013202. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_12"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Milano, M., Recto, R., Magrino, T., Myers, A.: A tour of Gallifrey, a language for geodistributed programming. In: Lerner, B.S., Bod\u00edk, R., Krishnamurthi, S. (eds.) 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0136, pp. 11:1\u201311:19. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl (2019). https:\/\/doi.org\/10.4230\/LIPIcs.SNAPL.2019.11","DOI":"10.4230\/LIPIcs.SNAPL.2019.11"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Nguyen, D.T., Beringer, L., Mansky, W., Wang, S.: Compositional verification of concurrent C programs with search structure templates. In: CPP (2024)","DOI":"10.1145\/3636501.3636940"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Padon, O.: Deductive verification of distributed protocols in first-order logic. In: FMCAD (2018)","DOI":"10.23919\/FMCAD.2018.8603010"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: Decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA), 1\u201331 (2017)","DOI":"10.1145\/3140568"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Recio, R.J., Culley, P.R., Garcia, D., Metzler, B., Hilland, J.: A remote direct memory access protocol specification. RFC 5040 (2007). https:\/\/doi.org\/10.17487\/RFC5040, https:\/\/www.rfc-editor.org\/info\/rfc5040","DOI":"10.17487\/RFC5040"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P da Rocha Pinto","year":"2014","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207\u2013231. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Sammler, M., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., Garg, D.: RefinedC: automating the foundational verification of C code with refined ownership types. In: PLDI (2021)","DOI":"10.1145\/3453483.3454036"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2(POPL), 1\u201330 (2017)","DOI":"10.1145\/3158116"},{"key":"6_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-24550-3_29","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"M Shapiro","year":"2011","unstructured":"Shapiro, M., Pregui\u00e7a, N., Baquero, C., Zawirski, M.: Conflict-free replicated data types. In: D\u00e9fago, X., Petit, F., Villain, V. (eds.) SSS 2011. LNCS, vol. 6976, pp. 386\u2013400. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24550-3_29"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Sharma, U., Jung, R., Tassarotti, J., Kaashoek, M.F., Zeldovich, N.: Grove: a separation-logic library for verifying distributed systems. In: SOSP (2023)","DOI":"10.1145\/3600006.3613172"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Song, W., et al.: Cascade: an edge computing platform for real-time machine intelligence. In: ApPLIED 2022 (2022)","DOI":"10.1145\/3524053.3542741"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Timany, A., et al.: Trillium: higher-order concurrent and distributed separation logic for intensional refinement. Proc. ACM Program. Lang. 8(POPL), 241\u2013272 (2024)","DOI":"10.1145\/3632851"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. In: PLDI (2015)","DOI":"10.1145\/2737924.2737958"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.E.: Planning for change in a formal verification of the raft consensus protocol. In: CPP (2016)","DOI":"10.1145\/2854065.2854081"},{"issue":"2","key":"6_CR42","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1109\/TKDE.2019.2898401","volume":"33","author":"C Wu","year":"2021","unstructured":"Wu, C., Faleiro, J.M., Lin, Y., Hellerstein, J.M.: Anna: a KVS for any scale. IEEE Trans. Knowl. Data Eng. 33(2), 344\u2013358 (2021). https:\/\/doi.org\/10.1109\/TKDE.2019.2898401","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"Xia, L., et al.: Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4(POPL), 1\u201332 (2020)","DOI":"10.1145\/3371119"},{"issue":"12","key":"6_CR44","doi-asserted-by":"publisher","first-page":"1144","DOI":"10.1109\/TSE.2017.2655056","volume":"43","author":"P Zave","year":"2017","unstructured":"Zave, P.: Reasoning about identifier spaces: How to make Chord correct. IEEE Trans. Software Eng. 43(12), 1144\u20131156 (2017)","journal-title":"IEEE Trans. Software Eng."},{"key":"6_CR45","unstructured":"Zhang, H., et al.: Verifying an HTTP Key-Value Server with Interaction Trees and VST. In: ITP (2021)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-60698-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,20]],"date-time":"2024-11-20T01:23:14Z","timestamp":1732065794000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-60698-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031606977","9783031606984"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-60698-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}