{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T01:02:56Z","timestamp":1769043776909,"version":"3.49.0"},"publisher-location":"Cham","reference-count":47,"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>We consider the verification of liveness properties for concurrent programs running on weak memory models. To that end, we identify notions of fairness that preclude demonic non-determinism, are motivated by practical observations, and are amenable to algorithmic techniques. We provide both logical and stochastic definitions of our fairness notions, and prove that they are equivalent in the context of liveness verification. In particular, we show that our fairness allows us to reduce the liveness problem (repeated control state reachability) to the problem of simple control state reachability. We show that this is a general phenomenon by developing a uniform framework which serves as the formal foundation of our fairness definition, and can be instantiated to a wide landscape of memory models. These models include SC, TSO, PSO, (Strong\/Weak) Release-Acquire, Strong Coherence, FIFO-consistency, and RMO.<\/jats:p>","DOI":"10.1007\/978-3-031-37706-8_10","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"184-205","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Overcoming Memory Weakness with\u00a0Unified Fairness"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8229-3481","authenticated-orcid":false,"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7704-304X","authenticated-orcid":false,"given":"Adwait","family":"Godbole","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0925-398X","authenticated-orcid":false,"given":"Shankaranarayanan","family":"Krishna","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-5709-899X","authenticated-orcid":false,"given":"Mihir","family":"Vahanwala","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-72019-3_1","volume-title":"Programming Languages and Systems","author":"PA Abdulla","year":"2021","unstructured":"Abdulla, P.A., Atig, M.F., Godbole, A., Krishna, S., Vafeiadis, V.: The decidability of verification under PS 2.0. In: ESOP 2021. LNCS, vol. 12648, pp. 1\u201329. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_1"},{"issue":"4","key":"10_CR2","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2178\/bsl\/1294171129","volume":"16","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bull. Symb. Log. 16(4), 457\u2013515 (2010). https:\/\/doi.org\/10.2178\/bsl\/1294171129","journal-title":"Bull. Symb. Log."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Source sets: a foundation for optimal dynamic partial order reduction. J. ACM 64(4), 25:1\u201325:49 (2017)","DOI":"10.1145\/3073408"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-030-99336-8_12","volume-title":"Programming Languages and Systems","author":"PA Abdulla","year":"2022","unstructured":"Abdulla, P.A., Atig, M.F., Agarwal, R.A., Godbole, A., S., K.: Probabilistic total store ordering. In: ESOP 2022. LNCS, vol. 13240, pp. 317\u2013345. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_12"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Agarwal, R.A., Godbole, A., Krishna, S.: Probabilistic total store ordering (2022). https:\/\/arxiv.org\/abs\/2201.10213","DOI":"10.1007\/978-3-030-99336-8_12"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Godbole, A., Krishna, S., Vahanwala, M.: Overcoming memory weakness with unified fairness (2023). https:\/\/arxiv.org\/abs\/2305.17605","DOI":"10.1007\/978-3-031-37706-8_10"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Henda, N.B., Mayr, R.: Decisive markov chains. LMCS 3(4) (2007)","DOI":"10.2168\/LMCS-3(4:7)2007"},{"issue":"12","key":"10_CR8","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"SV Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. IEEE Comput. 29(12), 66\u201376 (1996)","journal-title":"IEEE Comput."},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/s10703-012-0161-5","volume":"41","author":"J Alglave","year":"2012","unstructured":"Alglave, J.: A formal hierarchy of weak memory models. Formal Methods Syst. Des. 41, 178\u2013210 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data-mining for weak memory. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (2014)","DOI":"10.1145\/2594291.2594347"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-540-32275-7_14","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B Aminof","year":"2005","unstructured":"Aminof, B., Ball, T., Kupferman, O.: Reasoning about systems with transition fairness. In: Baader, F., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3452, pp. 194\u2013208. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_14"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17\u201323 January 2010, pp. 7\u201318 (2010). https:\/\/doi.org\/10.1145\/1706299.1706303","DOI":"10.1145\/1706299.1706303"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"MF Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 99\u2013115. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_9"},{"key":"10_CR14","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing c++ concurrency. In: ACM-SIGACT Symposium on Principles of Programming Languages (2011)","DOI":"10.1145\/1926385.1926394"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 392\u2013403. Association for Computing Machinery, New York (2009). https:\/\/doi.org\/10.1145\/1480881.1480930","DOI":"10.1145\/1480881.1480930"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-030-31784-3_27","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2019","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Ku\u010dera, A., Novotn\u00fd, P., Velan, D.: Deciding fast termination for probabilistic VASS with nondeterminism. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 462\u2013478. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_27"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Kiefer, S., Kucera, A., Novotn\u00fd, P., Katoen, J.: Zero-reachability in probabilistic multi-counter automata. In: Henzinger, T.A., Miller, D. (eds.) Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, Vienna, Austria, 14\u201318 July 2014, pp. 22:1\u201322:10. ACM (2014). https:\/\/doi.org\/10.1145\/2603088.2603161","DOI":"10.1145\/2603088.2603161"},{"issue":"1","key":"10_CR19","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1016\/j.jcss.2014.06.005","volume":"81","author":"T Br\u00e1zdil","year":"2015","unstructured":"Br\u00e1zdil, T., Kiefer, S., Kucera, A., Varekov\u00e1, I.H.: Runtime analysis of probabilistic programs with unbounded recursion. J. Comput. Syst. Sci. 81(1), 288\u2013310 (2015). https:\/\/doi.org\/10.1016\/j.jcss.2014.06.005","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Broy, M., Wirsing, M.: On the algebraic specification of nondeterministic programming languages. In: CAAP (1981)","DOI":"10.1007\/3-540-10828-9_61"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Chakraborty, S., Vafeiadis, V.: Grounding thin-air reads with event structures. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290383","DOI":"10.1145\/3290383"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Doherty, S., Dongol, B., Wehrheim, H., Derrick, J.: Verifying C11 programs operationally. In: Hollingsworth, J.K., Keidar, I. (eds.) Proceedings of the 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2019, Washington, DC, USA, 16\u201320 February 2019, pp. 355\u2013365. ACM (2019). https:\/\/doi.org\/10.1145\/3293883.3295702","DOI":"10.1145\/3293883.3295702"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Elver, M., Nagarajan, V.: Tso-cc: consistency directed cache coherence for tso. In: 2014 IEEE 20th International Symposium on High Performance Computer Architecture (HPCA), pp. 165\u2013176 (2014). https:\/\/doi.org\/10.1109\/HPCA.2014.6835927","DOI":"10.1109\/HPCA.2014.6835927"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kucera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), Turku, Finland, 14\u201317 July 2004, Proceedings, pp. 12\u201321. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/LICS.2004.1319596","DOI":"10.1109\/LICS.2004.1319596"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Etessami, K., Yannakakis, M.: Recursive markov decision processes and recursive stochastic games. J. ACM 62(2), 11:1\u201311:69 (2015). https:\/\/doi.org\/10.1145\/2699431","DOI":"10.1145\/2699431"},{"issue":"1\u20132","key":"10_CR26","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00102-X","journal-title":"Theor. Comput. Sci."},{"key":"10_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3329125","volume":"52","author":"RJ van Glabbeek","year":"2019","unstructured":"van Glabbeek, R.J., H\u00f6fner, P.: Progress, justness, and fairness. ACM Comput. Surv. (CSUR) 52, 1\u201338 (2019)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Jeffrey, A., Riely, J.: On thin air reads towards an event structures model of relaxed memory, pp. 759\u2013767 (2016). https:\/\/doi.org\/10.1145\/2933575.2934536","DOI":"10.1145\/2933575.2934536"},{"key":"10_CR29","unstructured":"Kaiser, J., Dang, H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: reasoning about release-acquire consistency in iris. In: Proceedings of the 31st European Conference on Object-Oriented Programming, ECOOP 2017, pp. 17:1\u201317:29 (2017)"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 175\u2013189. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3009837.3009850","DOI":"10.1145\/3009837.3009850"},{"issue":"1","key":"10_CR31","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10703-006-4342-y","volume":"28","author":"Y Kesten","year":"2006","unstructured":"Kesten, Y., Pnueli, A., Raviv, L., Shahar, E.: Model checking with strong fairness. Formal Methods Syst. Des. 28(1), 57\u201384 (2006). https:\/\/doi.org\/10.1007\/s10703-006-4342-y","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. PACMPL 2, 17:1\u201317:32 (2018)","DOI":"10.1145\/3158105"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"Lahav, O., Boker, U.: What\u2019s decidable about causally consistent shared memory? ACM Trans. Program. Lang. Syst. 44(2) (2022). https:\/\/doi.org\/10.1145\/3505273","DOI":"10.1145\/3505273"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. 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, 20\u201322 January 2016, pp. 649\u2013662. ACM (2016)","DOI":"10.1145\/2837614.2837643"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Lahav, O., Namakonov, E., Oberhauser, J., Podkopaev, A., Vafeiadis, V.: Making weak memory models fair. ArXiv arXiv:abs\/2012.01067 (2020)","DOI":"10.1145\/3485475"},{"key":"10_CR37","doi-asserted-by":"publisher","unstructured":"Lahav, O., Namakonov, E., Oberhauser, J., Podkopaev, A., Vafeiadis, V.: Making weak memory models fair (2020). https:\/\/doi.org\/10.48550\/ARXIV.2012.01067","DOI":"10.48550\/ARXIV.2012.01067"},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"Lahav, O., Vafeiadis, V.: Explaining relaxed memory models with program transformations. In: FM (2016)","DOI":"10.1007\/978-3-319-48989-6_29"},{"key":"10_CR39","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequential consistency in c\/c++11. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pp. 618\u2013632. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"10_CR40","doi-asserted-by":"crossref","unstructured":"Lamport, L.: How to make a multiprocessor that correctly executes multiprocess programs. IEEE Trans. Comput. C 28, 690\u2013691 (1979)","DOI":"10.1109\/TC.1979.1675439"},{"key":"10_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-642-31424-7_36","volume-title":"Computer Aided Verification","author":"S Mador-Haim","year":"2012","unstructured":"Mador-Haim, S., et al.: An axiomatic memory model for POWER multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 495\u2013512. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_36"},{"key":"10_CR42","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"10_CR43","doi-asserted-by":"publisher","unstructured":"Nienhuis, K., Memarian, K., Sewell, P.: An operational semantics for c\/c++11 concurrency. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, pp. 111\u2013128. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2983990.2983997","DOI":"10.1145\/2983990.2983997"},{"key":"10_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93\u2013107. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_7"},{"key":"10_CR45","doi-asserted-by":"publisher","unstructured":"Ros, A., Kaxiras, S.: Callback: efficient synchronization without invalidation with a directory just for spin-waiting. In: Proceedings of the 42nd Annual International Symposium on Computer Architecture, ISCA 2015, pp. 427\u2013438. Association for Computing Machinery, New York (2015). https:\/\/doi.org\/10.1145\/2749469.2750405","DOI":"10.1145\/2749469.2750405"},{"issue":"7","key":"10_CR46","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-tso: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"10_CR47","doi-asserted-by":"publisher","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: POPL, pp. 184\u2013193. ACM Press (1986). https:\/\/doi.org\/10.1145\/512644.512661","DOI":"10.1145\/512644.512661"}],"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_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T11:04:17Z","timestamp":1704452657000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37706-8_10"}},"subtitle":["Systematic Verification of Liveness in Weak Memory Models"],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377051","9783031377068"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37706-8_10","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)"}}]}}