{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:13:15Z","timestamp":1767928395309,"version":"3.49.0"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030449131","type":"print"},{"value":"9783030449148","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T00:00:00Z","timestamp":1587168000000},"content-version":"vor","delay-in-days":108,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Building network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present , a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the <jats:italic>two-phase-commit<\/jats:italic> protocol with a replicated logging service as a client. The two examples certify that  is well-suited for both horizontal and vertical modular reasoning.<\/jats:p>","DOI":"10.1007\/978-3-030-44914-8_13","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"336-365","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems"],"prefix":"10.1007","author":[{"given":"Morten","family":"Krogh-Jespersen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marit Edna","family":"Ohlenbusch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6045-5232","authenticated-orcid":false,"given":"Simon Oddershede","family":"Gregersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,18]]},"reference":[{"key":"13_CR1","unstructured":"Birkedal, L., Bizjak, A.: Lecture notes on Iris: Higher-order concurrent separation logic (2017), URL http:\/\/iris-project.org\/tutorial-pdfs\/iris-lecture-notes.pdf"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Deni\u00e9lou, P., Yoshida, N.: Dynamic multirole session types. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011, pp. 435\u2013446, ACM (2011), https:\/\/doi.org\/10.1145\/1926385.1926435","DOI":"10.1145\/1926385.1926435"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23\u201325, 2013, pp. 287\u2013300, ACM (2013), https:\/\/doi.org\/10.1145\/2429069.2429104","DOI":"10.1145\/2429069.2429104"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21\u201325, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6183, pp. 504\u2013528, Springer (2010), https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. Mathematical aspects of computer science 19(19\u201332), 1 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Gray, J.: Notes on data base operating systems. In: Flynn, M.J., Gray, J., Jones, A.K., Lagally, K., Opderbeck, H., Popek, G.J., Randell, B., Saltzer, J.H., Wiehle, H. (eds.) Operating Systems, An Advanced Course, Lecture Notes in Computer Science, vol. 60, pp. 393\u2013481, Springer (1978), https:\/\/doi.org\/10.1007\/3-540-08755-9_9","DOI":"10.1007\/3-540-08755-9_9"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving practical distributed systems correct. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4\u20137, 2015, pp. 1\u201317, ACM (2015), https:\/\/doi.org\/10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Hinrichsen, J.K., Bengtson, J., Krebbers, R.: Actris: session-type based reasoning in separation logic. PACMPL 4, 6:1\u20136:30 (2020), https:\/\/doi.org\/10.1145\/3371074","DOI":"10.1145\/3371074"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279\u2013295 (1997), https:\/\/doi.org\/10.1109\/32.588521","DOI":"10.1109\/32.588521"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C.(ed.) Programming Languages and Systems - ESOP\u201998, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201998, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, Lecture Notes in Computer Science, vol. 1381, pp. 122\u2013138. Springer (1998), https:\/\/doi.org\/10.1007\/BFb0053567","DOI":"10.1007\/BFb0053567"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7\u201312, 2008, pp. 273\u2013284, ACM (2008), https:\/\/doi.org\/10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Jung, R., Jourdan, J., Krebbers, R., Dreyer, D.: Rustbelt: securing the foundations of the rust programming language. PACMPL 2(POPL), 66:1\u201366:34 (2018), https:\/\/doi.org\/10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, p. 256\u2013269, ICFP 2016, Association for Computing Machinery, New York, NY, USA (2016), ISBN 9781450342193, https:\/\/doi.org\/10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"13_CR14","doi-asserted-by":"publisher","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), https:\/\/doi.org\/10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15\u201317, 2015, pp. 637\u2013650, ACM (2015), https:\/\/doi.org\/10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Kaiser, J., Dang, H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In: M\u00fcller, P. (ed.) 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19\u201323, 2017, Barcelona, Spain, LIPIcs, vol. 74, pp. 17:1\u201317:29, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017), https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2017.17","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Killian, C.E., Anderson, J.W., Braud, R., Jhala, R., Vahdat, A.: Mace: language support for building distributed systems. In: Ferrante, J., McKinley, K.S. (eds.) Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10\u201313, 2007, pp. 179\u2013188, ACM (2007), https:\/\/doi.org\/10.1145\/1250734.1250755","DOI":"10.1145\/1250734.1250755"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Krebbers, R., Jung, R., Bizjak, A., Jourdan, J., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22\u201329, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10201, pp. 696\u2013723, Springer (2017), https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18\u201320, 2017, pp. 205\u2013217, ACM (2017)","DOI":"10.1145\/3009837.3009855"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Krogh-Jespersen, M., Timany, A., Ohlenbusch, M.E., Gregersen, S.O., Birkedal, L.: Aneris: A mechanised logic for modular reasoning about distributed systems - technical appendix (2020), URL https:\/\/iris-project.org\/pdfs\/2020-esop-aneris-final-appendix.pdf","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2), 125\u2013143 (1977), https:\/\/doi.org\/10.1109\/TSE.1977.229904","DOI":"10.1109\/TSE.1977.229904"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Lamport, L.: The implementation of reliable distributed multiprocess systems. Computer Networks 2, 95\u2013114 (1978), https:\/\/doi.org\/10.1016\/0376-5075(78)90045-4","DOI":"10.1016\/0376-5075(78)90045-4"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Hybrid systems in TLA\n$${}^{\\text{+}}$$\n. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems, Lecture Notes in Computer Science, vol. 736, pp. 77\u2013102, Springer (1992), https:\/\/doi.org\/10.1007\/3-540-57318-6_25","DOI":"10.1007\/3-540-57318-6_25"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6355, pp. 348\u2013370, Springer (2010), https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Lesani, M., Bell, C.J., Chlipala, A.: Chapar: certified causally consistent distributed key-value stores. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20\u201322, 2016, pp. 357\u2013370, ACM (2016), https:\/\/doi.org\/10.1145\/2837614.2837622","DOI":"10.1145\/2837614.2837622"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Ley-Wild, R., Nanevski, A.: Subjective auxiliary state for coarse-grained concurrency. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23\u201325, 2013, pp. 561\u2013574, ACM (2013), https:\/\/doi.org\/10.1145\/2429069.2429134","DOI":"10.1145\/2429069.2429134"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A.: Communicating state transition systems for fine-grained concurrent resources. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014, Proceedings, Lecture Notes in Computer Science, vol. 8410, pp. 290\u2013310, Springer (2014), https:\/\/doi.org\/10.1007\/978-3-642-54833-8_16","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1\u20133), 271\u2013307 (2007), https:\/\/doi.org\/10.1016\/j.tcs.2006.12.035","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 46\u201357, IEEE Computer Society (1977), https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: Formal specification, verification, and implementation of fault-tolerant systems using EventML. ECEASST 72 (2015), https:\/\/doi.org\/10.14279\/tuj.eceasst.72.1013","DOI":"10.14279\/tuj.eceasst.72.1013"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems. Sci. Comput. Program. 148, 26\u201348 (2017), https:\/\/doi.org\/10.1016\/j.scico.2017.05.009","DOI":"10.1016\/j.scico.2017.05.009"},{"key":"13_CR32","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22\u201325 July 2002, Copenhagen, Denmark, Proceedings, pp. 55\u201374, IEEE Computer Society (2002), https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: Tada: A logic for time and data abstraction. In: Jones, R.E. (ed.) ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8586, pp. 207\u2013231, Springer (2014), https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Grove, D., Blackburn, S. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15\u201317, 2015, pp. 77\u201387, ACM (2015), https:\/\/doi.org\/10.1145\/2737924.2737964","DOI":"10.1145\/2737924.2737964"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. PACMPL 2(POPL), 28:1\u201328:30 (2018), https:\/\/doi.org\/10.1145\/3158116","DOI":"10.1145\/3158116"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014, Proceedings, Lecture Notes in Computer Science, vol. 8410, pp. 149\u2013168, Springer (2014), https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Timany, A., Stefanesco, L., Krogh-Jespersen, M., Birkedal, L.: A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. PACMPL 2(POPL), 64:1\u201364:28 (2018), https:\/\/doi.org\/10.1145\/3158152","DOI":"10.1145\/3158152"},{"key":"13_CR38","doi-asserted-by":"publisher","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Schneider-Kamp, P., Hanus, M. (eds.) Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20\u201322, 2011, Odense, Denmark, pp. 161\u2013172, ACM (2011), https:\/\/doi.org\/10.1145\/2003476.2003499","DOI":"10.1145\/2003476.2003499"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: Morrisett, G., Uustalu, T. (eds.) ACM SIGPLAN International Conference on Functional Programming, ICFP\u201913, Boston, MA, USA - September 25\u201327, 2013, pp. 377\u2013390, ACM (2013), https:\/\/doi.org\/10.1145\/2500365.2500600","DOI":"10.1145\/2500365.2500600"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.E.: Verdi: a framework for implementing and formally verifying distributed systems. In: Grove, D., Blackburn, S. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15\u201317, 2015, pp. 357\u2013368, ACM (2015), https:\/\/doi.org\/10.1145\/2737924.2737958","DOI":"10.1145\/2737924.2737958"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-44914-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T17:11:10Z","timestamp":1656609070000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-44914-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030449131","9783030449148"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-44914-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"18 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"87","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11-12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}