{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:17:04Z","timestamp":1767928624547,"version":"3.49.0"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","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,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"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 present a framework for efficient stateless model checking (SMC) of concurrent programs under three prominent models of causal consistency, <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\texttt {CCv}}, {\\texttt {CM}}, \\texttt{CC}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>CCv<\/mml:mi>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mi>CM<\/mml:mi>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mi>CC<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Our approach is based on exploring traces under the program order \"Image missing\" and the reads from \"Image missing\" relations. Our SMC algorithm is provably optimal in the sense that it explores each \"Image missing\" and \"Image missing\" relation exactly once. We have implemented our framework in a tool called <jats:sc>Conschecker<\/jats:sc>. Experiments show that <jats:sc>Conschecker<\/jats:sc> performs well in detecting anomalies in classical distributed databases benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_6","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T20:19:12Z","timestamp":1682108352000},"page":"105-125","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Optimal Stateless Model Checking for Causal Consistency"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh","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-0003-0925-398X","authenticated-orcid":false,"given":"S.","family":"Krishna","sequence":"additional","affiliation":[]},{"given":"Ashutosh","family":"Gupta","sequence":"additional","affiliation":[]},{"given":"Omkar","family":"Tuppe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. SIGPLAN Not. 49(1), 373\u2013384 (jan 2014). https:\/\/doi.org\/10.1145\/2578855.2535845, https:\/\/doi.org\/10.1145\/2578855.2535845","DOI":"10.1145\/2578855.2535845"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P., Atig, M.F., S, K., Gupta, A., Tuppe, O.: Optimal Stateless Model Checking for Causal Consistency (Jan 2023). https:\/\/doi.org\/10.5281\/zenodo.7572282, https:\/\/doi.org\/10.5281\/zenodo.7572282","DOI":"10.5281\/zenodo.7572282"},{"key":"6_CR3","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for tso and pso. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 353\u2013367. Springer Berlin Heidelberg, Berlin, Heidelberg (2015)"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., L\u00e5ng, M., Ngo, T.P., Sagonas, K.: Optimal stateless model checking for reads-from equivalence under sequential consistency. Proc. ACM Program. Lang. 3(OOPSLA) (Oct 2019). https:\/\/doi.org\/10.1145\/3360576, https:\/\/doi.org\/10.1145\/3360576","DOI":"10.1145\/3360576"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. Proc. ACM Program. Lang. 2(OOPSLA) (Oct 2018). https:\/\/doi.org\/10.1145\/3276505, https:\/\/doi.org\/10.1145\/3276505","DOI":"10.1145\/3276505"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., Toman, V.: Stateless model checking under a reads-value-from equivalence. In: Silva and Leino [43], pp. 341\u2013366. https:\/\/doi.org\/10.1007\/978-3-030-81685-8_16, https:\/\/doi.org\/10.1007\/978-3-030-81685-8_16","DOI":"10.1007\/978-3-030-81685-8_16"},{"key":"6_CR7","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 (Mar 1995). https:\/\/doi.org\/10.1007\/BF01784241, https:\/\/doi.org\/10.1007\/BF01784241","DOI":"10.1007\/BF01784241"},{"key":"6_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) (jul 2014). https:\/\/doi.org\/10.1145\/2627752, https:\/\/doi.org\/10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Bailis, P., Ghodsi, A., Hellerstein, J.M., Stoica, I.: Bolt-on causal consistency. In: Ross, K.A., Srivastava, D., Papadias, D. (eds.) Proceedings of the ACM SIGMOD International Conference on Management of Data, SIGMOD 2013, New York, NY, USA, June 22-27, 2013. pp. 761\u2013772. ACM (2013). https:\/\/doi.org\/10.1145\/2463676.2465279, https:\/\/doi.org\/10.1145\/2463676.2465279","DOI":"10.1145\/2463676.2465279"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. 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-28, 2011. pp. 55\u201366. ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926394, https:\/\/doi.org\/10.1145\/1926385.1926394","DOI":"10.1145\/1926385.1926394"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Checking robustness between weak transactional consistency models. Programming Languages and Systems 12648, \u00a087 (2021)","DOI":"10.1007\/978-3-030-72019-3_4"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Robustness Against Transactional Causal Consistency. Logical Methods in Computer Science Volume 17, Issue 1 (Feb 2021). https:\/\/doi.org\/10.23638\/LMCS-17(1:12)2021, https:\/\/lmcs.episciences.org\/7149","DOI":"10.23638\/LMCS-17(1:12)2021"},{"key":"6_CR13","unstructured":"Bernardi, G., Gotsman, A.: Robustness against consistency models with atomic visibility. In: 27th International Conference on Concurrency Theory (CONCUR 2016). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016)"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Biswas, R., Enea, C.: On the complexity of checking transactional consistency. Proc. ACM Program. Lang. 3(OOPSLA) (oct 2019). https:\/\/doi.org\/10.1145\/3360591, https:\/\/doi.org\/10.1145\/3360591","DOI":"10.1145\/3360591"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. p. 626\u2013638. POPL 2017, Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3009837.3009888, https:\/\/doi.org\/10.1145\/3009837.3009888","DOI":"10.1145\/3009837.3009888"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Burckhardt, S.: Principles of eventual consistency. Found. Trends Program. Lang. 1(1-2), 1\u2013150 (2014). https:\/\/doi.org\/10.1561\/2500000011, https:\/\/doi.org\/10.1561\/2500000011","DOI":"10.1561\/2500000011"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Christakis, M., Gotovos, A., Sagonas, K.: Systematic testing for detecting concurrency errors in erlang programs. In: Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, Luxembourg, March 18-22, 2013. pp. 154\u2013163. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/ICST.2013.50, https:\/\/doi.org\/10.1109\/ICST.2013.50","DOI":"10.1109\/ICST.2013.50"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.A.: State space reduction using partial order techniques. Int. J. Softw. Tools Technol. Transf. 2(3), 279\u2013287 (1999). https:\/\/doi.org\/10.1007\/s100090050035, https:\/\/doi.org\/10.1007\/s100090050035","DOI":"10.1007\/s100090050035"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Difallah, D.E., Pavlo, A., Curino, C., Cudre-Mauroux, P.: Oltp-bench: An extensible testbed for benchmarking relational databases. Proc. VLDB Endow. 7(4), 277\u2013288 (dec 2013). https:\/\/doi.org\/10.14778\/2732240.2732246, https:\/\/doi.org\/10.14778\/2732240.2732246","DOI":"10.14778\/2732240.2732246"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Du, J., Elnikety, S., Roy, A., Zwaenepoel, W.: Orbe: scalable causal consistency using dependency matrices and physical clocks. In: Lohman, G.M. (ed.) ACM Symposium on Cloud Computing, SOCC \u201913, Santa Clara, CA, USA, October 1-3, 2013. pp. 11:1\u201311:14. ACM (2013). https:\/\/doi.org\/10.1145\/2523616.2523628, https:\/\/doi.org\/10.1145\/2523616.2523628","DOI":"10.1145\/2523616.2523628"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Du, J., Iorgulescu, C., Roy, A., Zwaenepoel, W.: Gentlerain: Cheap and scalable causal consistency with physical clocks. In: Lazowska, E., Terry, D., Arpaci-Dusseau, R.H., Gehrke, J. (eds.) Proceedings of the ACM Symposium on Cloud Computing, Seattle, WA, USA, November 3-5, 2014. pp. 4:1\u20134:13. ACM (2014). https:\/\/doi.org\/10.1145\/2670979.2670983, https:\/\/doi.org\/10.1145\/2670979.2670983","DOI":"10.1145\/2670979.2670983"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, Lecture Notes in Computer Science, vol.\u00a01032. Springer (1996). https:\/\/doi.org\/10.1007\/3-540-60761-7, https:\/\/doi.org\/10.1007\/3-540-60761-7","DOI":"10.1007\/3-540-60761-7"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 174\u2013186. POPL \u201997, Association for Computing Machinery, New York, NY, USA (1997). https:\/\/doi.org\/10.1145\/263699.263717, https:\/\/doi.org\/10.1145\/263699.263717","DOI":"10.1145\/263699.263717"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Software model checking: The verisoft approach. Form. Methods Syst. Des. 26(2), 77\u2013101 (Mar 2005). https:\/\/doi.org\/10.1007\/s10703-005-1489-x, https:\/\/doi.org\/10.1007\/s10703-005-1489-x","DOI":"10.1007\/s10703-005-1489-x"},{"key":"6_CR25","unstructured":"Hamza, J.: Algorithmic Verification of Concurrent and Distributed Data Structures. Ph.D. thesis, Universit\u00e9 Paris Diderot (2015)"},{"key":"6_CR26","doi-asserted-by":"publisher","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990). https:\/\/doi.org\/10.1145\/78969.78972, https:\/\/doi.org\/10.1145\/78969.78972","DOI":"10.1145\/78969.78972"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Holt, B., Bornholt, J., Zhang, I., Ports, D., Oskin, M., Ceze, L.: Disciplined inconsistency with consistency types. In: Proceedings of the Seventh ACM Symposium on Cloud Computing. p. 279\u2013293. SoCC \u201916, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2987550.2987559, https:\/\/doi.org\/10.1145\/2987550.2987559","DOI":"10.1145\/2987550.2987559"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. Proc. ACM Program. Lang. 2(POPL), 17:1\u201317:32 (2018). https:\/\/doi.org\/10.1145\/3158105, https:\/\/doi.org\/10.1145\/3158105","DOI":"10.1145\/3158105"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Marmanis, I., Gladstein, V., Vafeiadis, V.: Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang. 6(POPL), 1\u201328 (2022). https:\/\/doi.org\/10.1145\/3498711, https:\/\/doi.org\/10.1145\/3498711","DOI":"10.1145\/3498711"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Vafeiadis, V.: Genmc: A model checker for weak memory models. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification. pp. 427\u2013440. Springer International Publishing, Cham (2021)","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"6_CR31","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, https:\/\/doi.org\/10.1145\/3326938.3326942","DOI":"10.1145\/3326938.3326942"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978). https:\/\/doi.org\/10.1145\/359545.359563, https:\/\/doi.org\/10.1145\/359545.359563","DOI":"10.1145\/359545.359563"},{"key":"6_CR33","doi-asserted-by":"publisher","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers 28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439, https:\/\/doi.org\/10.1109\/TC.1979.1675439","DOI":"10.1109\/TC.1979.1675439"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz, A.: Trace theory. In: Advances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to Other Models of Concurrency. p. 279\u2013324. Springer-Verlag, Berlin, Heidelberg (1987)","DOI":"10.1007\/3-540-17906-2_30"},{"key":"6_CR35","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. pp. 267\u2013280. USENIX Association (2008), http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/musuvathi\/musuvathi.pdf"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"Nair, S.S., Petri, G., Shapiro, M.: Proving the safety of highly-available distributed objects. In: M\u00fcller, P. (ed.) Programming Languages and Systems. pp. 544\u2013571. Springer International Publishing, Cham (2020)","DOI":"10.1007\/978-3-030-44914-8_20"},{"key":"6_CR37","doi-asserted-by":"publisher","unstructured":"Norris, B., Demsky, B.: A practical approach for model checking c\/c++11 code. ACM Trans. Program. Lang. Syst. 38(3) (May 2016). https:\/\/doi.org\/10.1145\/2806886, https:\/\/doi.org\/10.1145\/2806886","DOI":"10.1145\/2806886"},{"key":"6_CR38","doi-asserted-by":"publisher","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-tso. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05674, pp. 391\u2013407. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27, https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"6_CR39","doi-asserted-by":"publisher","unstructured":"Perrin, M., Most\u00e9faoui, A., Jard, C.: Causal consistency: beyond memory. In: Asenjo, R., Harris, T. (eds.) Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, Barcelona, Spain, March 12-16, 2016. pp. 26:1\u201326:12. ACM (2016). https:\/\/doi.org\/10.1145\/2851141.2851170, https:\/\/doi.org\/10.1145\/2851141.2851170","DOI":"10.1145\/2851141.2851170"},{"key":"6_CR40","doi-asserted-by":"publisher","unstructured":"Raynal, M., Schiper, A.: From causal consistency to sequential consistency in shared memory systems. In: Thiagarajan, P.S. (ed.) Foundations of Software Technology and Theoretical Computer Science, 15th Conference, Bangalore, India, December 18-20, 1995, Proceedings. Lecture Notes in Computer Science, vol.\u00a01026, pp. 180\u2013194. Springer (1995). https:\/\/doi.org\/10.1007\/3-540-60692-0_48, https:\/\/doi.org\/10.1007\/3-540-60692-0_48","DOI":"10.1007\/3-540-60692-0_48"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Proceedings of the 2nd International Haifa Verification Conference on Hardware and Software, Verification and Testing. p. 166\u2013182. HVC\u201906, Springer-Verlag, Berlin, Heidelberg (2006)","DOI":"10.1007\/978-3-540-70889-6_13"},{"key":"6_CR42","doi-asserted-by":"publisher","unstructured":"Shasha, D.E., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10(2), 282\u2013312 (1988). https:\/\/doi.org\/10.1145\/42190.42277, https:\/\/doi.org\/10.1145\/42190.42277","DOI":"10.1145\/42190.42277"},{"key":"6_CR43","doi-asserted-by":"publisher","unstructured":"Silva, A., Leino, K.R.M. (eds.): Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, Lecture Notes in Computer Science, vol. 12759. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8, https:\/\/doi.org\/10.1007\/978-3-030-81685-8","DOI":"10.1007\/978-3-030-81685-8"},{"key":"6_CR44","unstructured":"SV-COMP: Competition on Software Verification. https:\/\/sv-comp.sosy-lab.org\/2018 (2018), [Online; accessed 2017-11-10]"},{"key":"6_CR45","doi-asserted-by":"publisher","unstructured":"Tuppe, O.: Conschecker (Jan 2023). https:\/\/doi.org\/10.5281\/zenodo.7500551, https:\/\/doi.org\/10.5281\/zenodo.7500551","DOI":"10.5281\/zenodo.7500551"},{"key":"6_CR46","doi-asserted-by":"publisher","unstructured":"Zhang, N., Kusano, M., Wang, C.: Dynamic partial order reduction for relaxed memory models. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 250\u2013259. PLDI \u201915, Association for Computing Machinery, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2737924.2737956, https:\/\/doi.org\/10.1145\/2737924.2737956","DOI":"10.1145\/2737924.2737956"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,4]],"date-time":"2023-08-04T10:02:57Z","timestamp":1691143377000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_6","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":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","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":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","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":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","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":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","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":"56","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":"6","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":"33% - 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)"}}]}}