{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:11Z","timestamp":1779087671845,"version":"3.51.4"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377051","type":"print"},{"value":"9783031377068","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Rely-guarantee (RG) is a highly influential compositional proof technique for concurrent programs, which was originally developed assuming a sequentially consistent shared memory. In this paper, we first generalize RG to make it parametric with respect to the underlying memory model by introducing an RG framework that is applicable to any model axiomatically characterized by Hoare triples. Second, we instantiate this framework for reasoning about concurrent programs under <jats:italic>causally consistent memory<\/jats:italic>, which is formulated using a recently proposed <jats:italic>potential-based<\/jats:italic> operational semantics, thereby providing the first reasoning technique for such semantics. The proposed program logic, which we call <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf{Piccolo}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>Piccolo<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, employs a novel assertion language allowing one to specify ordered sequences of states that each thread may reach. We employ <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf{Piccolo}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>Piccolo<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> for multiple litmus tests, as well as for an adaptation of Peterson\u2019s algorithm for mutual exclusion to causally consistent memory.<\/jats:p>","DOI":"10.1007\/978-3-031-37706-8_11","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"206-229","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Rely-Guarantee Reasoning for\u00a0Causally Consistent Shared Memory"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2385-7512","authenticated-orcid":false,"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Arora, J., Atig, M.F., Krishna, S.N.: Verification of programs under the release-acquire semantics. In: PLDI, pp. 1117\u20131132. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314649","DOI":"10.1145\/3314221.3314649"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Kumar, K.N., Saivasan, P.: Deciding reachability under persistent x86-TSO. Proc. ACM Program. Lang. 5(POPL), 1\u201332 (2021). https:\/\/doi.org\/10.1145\/3434337","DOI":"10.1145\/3434337"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Verifying reachability for TSO programs with dynamic thread creation. In: Koulali, M.A., Mezini, M. (eds.) Networked Systems, NETYS 2022. LNCS, vol. 13464. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17436-0_19","DOI":"10.1007\/978-3-031-17436-0_19"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: The benefits of duality in verifying concurrent programs under TSO. In: CONCUR. LIPIcs, vol. 59, pp. 5:1\u20135:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.5","DOI":"10.4230\/LIPIcs.CONCUR.2016.5"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: A load-buffer semantics for total store ordering. Log. Methods Comput. Sci. 14(1) (2018). https:\/\/doi.org\/10.23638\/LMCS-14(1:9)2018","DOI":"10.23638\/LMCS-14(1:9)2018"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Ahamad, M., Neiger, G., Burns, J.E., Kohli, P., Hutto, P.W.: Causal memory: definitions, implementation, and programming. Distrib. Comput. 9(1), 37\u201349 (1995). https:\/\/doi.org\/10.1007\/BF01784241","DOI":"10.1007\/BF01784241"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Alglave, J., Cousot, P.: Ogre and Pythia: an invariance proof method for weak consistency models. In: Castagna, G., Gordon, A.D. (eds.) POPL, pp. 3\u201318. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009883","DOI":"10.1145\/3009837.3009883"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1\u20137:74 (2014). https:\/\/doi.org\/10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.: Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-1-84882-745-5","DOI":"10.1007\/978-1-84882-745-5"},{"key":"11_CR10","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Robustness against transactional causal consistency. Log. Meth. Comput. Sci. 17(1) (2021). http:\/\/lmcs.episciences.org\/7149"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-030-99336-8_9","volume-title":"Programming Languages and Systems","author":"EV Bila","year":"2022","unstructured":"Bila, E.V., Dongol, B., Lahav, O., Raad, A., Wickerson, J.: View-based Owicki\u2013Gries reasoning for persistent x86-TSO. In: ESOP 2022. LNCS, vol. 13240, pp. 234\u2013261. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_9"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. In: POPL, pp. 626\u2013638. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009888","DOI":"10.1145\/3009837.3009888"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991). https:\/\/doi.org\/10.1016\/0020-0190(91)90122-X","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-030-90870-6_16","volume-title":"Formal Methods","author":"N Coughlin","year":"2021","unstructured":"Coughlin, N., Winter, K., Smith, G.: Rely\/guarantee reasoning for multicopy atomic weak memory models. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 292\u2013310. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_16"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Coughlin, N., Winter, K., Smith, G.: Compositional reasoning for non-multicopy atomic architectures. Form. Asp. Comput. (2022). https:\/\/doi.org\/10.1145\/3574137","DOI":"10.1145\/3574137"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Dalvandi, S., Doherty, S., Dongol, B., Wehrheim, H.: Owicki-Gries reasoning for C11 RAR. In: ECOOP. LIPIcs, vol. 166, pp. 11:1\u201311:26. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2020.11","DOI":"10.4230\/LIPIcs.ECOOP.2020.11"},{"key":"11_CR17","doi-asserted-by":"publisher","unstructured":"Dalvandi, S., Dongol, B., Doherty, S., Wehrheim, H.: Integrating Owicki-Gries for C11-style memory models into Isabelle\/HOL. J. Autom. Reason. 66(1), 141\u2013171 (2022). https:\/\/doi.org\/10.1007\/s10817-021-09610-2","DOI":"10.1007\/s10817-021-09610-2"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL, pp. 287\u2013300. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429104","DOI":"10.1145\/2429069.2429104"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Doherty, S., Dalvandi, S., Dongol, B., Wehrheim, H.: Unifying operational weak memory verification: an axiomatic approach. ACM Trans. Comput. Log. 23(4), 27:1\u201327:39 (2022). https:\/\/doi.org\/10.1145\/3545117","DOI":"10.1145\/3545117"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Doherty, S., Dongol, B., Wehrheim, H., Derrick, J.: Verifying C11 programs operationally. In: PPoPP, pp. 355\u2013365. ACM (2019). https:\/\/doi.org\/10.1145\/3293883.3295702","DOI":"10.1145\/3293883.3295702"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983). https:\/\/doi.org\/10.1145\/69575.69577","DOI":"10.1145\/69575.69577"},{"key":"11_CR22","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":"11_CR23","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: ECOOP. LIPIcs, vol. 74, pp. 17:1\u201317:29. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2017.17","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Kan, S., Lin, A.W., R\u00fcmmer, P., Schrader, M.: CertiStr: a certified string solver. In: CPP, pp. 210\u2013224. ACM (2022). https:\/\/doi.org\/10.1145\/3497775.3503691","DOI":"10.1145\/3497775.3503691"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Kang, J., Hur, C., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: POPL, pp. 175\u2013189. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009850","DOI":"10.1145\/3009837.3009850"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Lahav, O.: Verification under causally consistent shared memory. ACM SIGLOG News 6(2), 43\u201356 (2019). https:\/\/doi.org\/10.1145\/3326938.3326942","DOI":"10.1145\/3326938.3326942"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Lahav, O., Boker, U.: Decidable verification under a causally consistent shared memory. In: PLDI, pp. 211\u2013226. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385966","DOI":"10.1145\/3385412.3385966"},{"key":"11_CR28","doi-asserted-by":"publisher","unstructured":"Lahav, O., Boker, U.: What\u2019s decidable about causally consistent shared memory? ACM Trans. Program. Lang. Syst. 44(2), 8:1\u20138:55 (2022). https:\/\/doi.org\/10.1145\/3505273","DOI":"10.1145\/3505273"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Lahav, O., Dongol, B., Wehrheim, H.: Artifact: rely-guarantee reasoning for causally consistent shared memory. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7929646","DOI":"10.5281\/zenodo.7929646"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Lahav, O., Dongol, B., Wehrheim, H.: Rely-guarantee reasoning for causally consistent shared memory (extended version) (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.08486","DOI":"10.48550\/arXiv.2305.08486"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: POPL, pp. 649\u2013662. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837643","DOI":"10.1145\/2837614.2837643"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-662-47666-6_25","volume-title":"Automata, Languages, and Programming","author":"O Lahav","year":"2015","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311\u2013323. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_25"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439","DOI":"10.1109\/TC.1979.1675439"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"de Le\u00f3n, H.P., Furbach, F., Heljanko, K., Meyer, R.: BMC with memory models as modules. In: FMCAD, pp. 1\u20139. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603021","DOI":"10.23919\/FMCAD.2018.8603021"},{"key":"11_CR35","doi-asserted-by":"publisher","unstructured":"Moszkowski, B.C.: A complete axiom system for propositional interval temporal logic with infinite time. Log. Meth. Comput. Sci. 8(3) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(3:10)2012","DOI":"10.2168\/LMCS-8(3:10)2012"},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391\u2013407. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27"},{"key":"11_CR37","doi-asserted-by":"publisher","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319\u2013340 (1976). https:\/\/doi.org\/10.1007\/BF00268134","DOI":"10.1007\/BF00268134"},{"issue":"3","key":"11_CR38","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"11_CR39","doi-asserted-by":"publisher","unstructured":"Raad, A., Lahav, O., Vafeiadis, V.: Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. Proc. ACM Program. Lang. 4(OOPSLA), 151:1\u2013151:28 (2020). https:\/\/doi.org\/10.1145\/3428219","DOI":"10.1145\/3428219"},{"key":"11_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-15057-9_4","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T Ridge","year":"2010","unstructured":"Ridge, T.: A rely-guarantee proof system for x86-TSO. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 55\u201370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15057-9_4"},{"key":"11_CR41","doi-asserted-by":"publisher","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Pf\u00e4hler, J., Reif, W.: RGITL: a temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. 71(1\u20133), 131\u2013174 (2014). https:\/\/doi.org\/10.1007\/s10472-013-9389-z","DOI":"10.1007\/s10472-013-9389-z"},{"key":"11_CR42","doi-asserted-by":"publisher","unstructured":"Sheng, Y., et al.: Reasoning about vectors using an SMT theory of sequences. In: Blanchette, J., Kov\u00e1ics, L., Pattinson, D. (eds.) Automated Reasoning, IJCAR 2022. LNCS, vol. 13385, pp. pp. 125\u2013143. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_9","DOI":"10.1007\/978-3-031-10769-6_9"},{"key":"11_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-89884-1_13","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2018","unstructured":"Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O., Vafeiadis, V.: A separation logic for a promising semantics. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 357\u2013384. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_13"},{"key":"11_CR44","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge, UK (2008). https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.612221"},{"key":"11_CR45","doi-asserted-by":"publisher","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: OOPSLA, pp. 867\u2013884. ACM (2013). https:\/\/doi.org\/10.1145\/2509136.2509532","DOI":"10.1145\/2509136.2509532"},{"key":"11_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256\u2013271. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_18"},{"key":"11_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-030-90870-6_13","volume-title":"Formal Methods","author":"D Wright","year":"2021","unstructured":"Wright, D., Batty, M., Dongol, B.: Owicki-Gries reasoning for C11 programs with relaxed dependencies. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 237\u2013254. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_13"},{"key":"11_CR48","doi-asserted-by":"publisher","unstructured":"Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput. 9(2), 149\u2013174 (1997). https:\/\/doi.org\/10.1007\/BF01211617","DOI":"10.1007\/BF01211617"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37706-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T11:05:33Z","timestamp":1704452733000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37706-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377051","9783031377068"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37706-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"26% - 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","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","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)"}}]}}