{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:46:49Z","timestamp":1777348009863,"version":"3.51.4"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131875","type":"print"},{"value":"9783031131882","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Reasoning about data structures requires powerful logics supporting the combination of structural and data properties. We define a new logic called <jats:sc>Mso-D<\/jats:sc><jats:italic>(Monadic Second-Order logic with Data)<\/jats:italic> as an extension of standard <jats:sc>Mso<\/jats:sc> on trees with predicates of the desired data logic. We also define a new class of <jats:italic>symbolic data tree automata<\/jats:italic> (<jats:sc>Sdta<\/jats:sc>s) to deal with data trees using a simple machine. <jats:sc>Mso-D<\/jats:sc> and <jats:sc>Sdta<\/jats:sc>s are both Turing-powerful, and their high expressiveness is necessary to deal with interesting data structures. We cope with undecidability by encoding <jats:sc>Sdta<\/jats:sc> executions as a system of CHCs <jats:italic>(Constrained Horn Clauses)<\/jats:italic>, and solving the resulting system using off-the-shelf solvers. We also identify a fragment of <jats:sc>Mso-D<\/jats:sc> whose satisfiability can be effectively reduced to the emptiness problem for <jats:sc>Sdta<\/jats:sc>s. This fragment is very expressive since it allows us to characterize a variety of data trees from the literature, solving certain infinite-state games, etc. We implement this reduction in a prototype tool that combines an <jats:sc>Mso<\/jats:sc> decision procedure over trees (<jats:sc>Mona<\/jats:sc>) with a CHC engine (Z3), and use this tool to conduct several experiments, demonstrating the effectiveness of our approach across different problem domains.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_13","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"249-271","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Reasoning About Data Trees Using CHCs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7617-5489","authenticated-orcid":false,"given":"Marco","family":"Faella","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8697-2980","authenticated-orcid":false,"given":"Gennaro","family":"Parlato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Beyene, T., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: POPL 2014, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 221\u2013233 (2014)","DOI":"10.1145\/2535838.2535860"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-642-33475-7_5","volume-title":"Theoretical Computer Science","author":"MHL Bodlaender","year":"2012","unstructured":"Bodlaender, M.H.L., Hurkens, C.A.J., Kusters, V.J.J., Staals, F., Woeginger, G.J., Zantema, H.: Cinderella versus the wicked stepmother. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 57\u201371. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33475-7_5"},{"issue":"1\u20136","key":"13_CR4","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"JR B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Math. Log. Q. 6(1\u20136), 66\u201392 (1960)","journal-title":"Math. Log. Q."},{"key":"13_CR5","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second-order arithmetic. In: Proceedings of 1960 International Congress for Logic, Methodology and Philosophy of Science, pp. 1\u201311. Stanford University Press (1962)"},{"issue":"7","key":"13_CR6","doi-asserted-by":"publisher","first-page":"1393","DOI":"10.1007\/s10817-020-09571-y","volume":"64","author":"A Champion","year":"2020","unstructured":"Champion, A., Chiba, T., Kobayashi, N., Sato, R.: Ice-based refinement type discovery for higher-order functional programs. J. Autom. Reason. 64(7), 1393\u20131418 (2020)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"13_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-11(3:10)2015","volume":"11","author":"T Colcombet","year":"2015","unstructured":"Colcombet, T., Ley, C., Puppis, G.: Logics with rigidly guarded data tests. Log. Methods Comput. Sci. 11(3), 1\u201356 (2015). https:\/\/doi.org\/10.2168\/LMCS-11(3:10)2015","journal-title":"Log. Methods Comput. Sci."},{"key":"13_CR8","unstructured":"Comon, H., et al.: Tree Automata Techniques and Applications (2008). https:\/\/hal.inria.fr\/hal-03367725"},{"key":"13_CR9","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)","edition":"3"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-25540-4_1","volume-title":"Computer Aided Verification","author":"L D\u2019Antoni","year":"2019","unstructured":"D\u2019Antoni, L., Ferreira, T., Sammartino, M., Silva, A.: Symbolic register automata. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 3\u201321. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_1"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Monadic second-order logic on finite sequences. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 232\u2013245. ACM (2017)","DOI":"10.1145\/3009837.3009844"},{"issue":"5","key":"13_CR12","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3419404","volume":"64","author":"L D\u2019Antoni","year":"2021","unstructured":"D\u2019Antoni, L., Veanes, M.: Automata modulo theories. Commun. ACM 64(5), 86\u201395 (2021)","journal-title":"Commun. ACM"},{"issue":"3","key":"13_CR13","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380\u2013415 (2007)","journal-title":"Inf. Comput."},{"issue":"5","key":"13_CR14","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1016\/S0022-0000(70)80041-1","volume":"4","author":"J Doner","year":"1970","unstructured":"Doner, J.: Tree acceptors and some of their applications. J. Comput. Syst. Sci. 4(5), 406\u2013451 (1970)","journal-title":"J. Comput. Syst. Sci."},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1090\/S0002-9947-1961-0139530-9","volume":"98","author":"CC Elgot","year":"1961","unstructured":"Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Am. Math. Soc. 98, 21\u201351 (1961)","journal-title":"Trans. Am. Math. Soc."},{"issue":"4","key":"13_CR16","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/321978.321991","volume":"23","author":"MH van Emden","year":"1976","unstructured":"van Emden, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. J. ACM 23(4), 733\u2013742 (1976)","journal-title":"J. ACM"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Strategy synthesis for linear arithmetic games. POPL. Proc. ACM Program. Lang. 2, 61:1\u201361:30 (2018)","DOI":"10.1145\/3158149"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Ahmad, M.B.S., Bod\u00edk, R.: Gradual synthesis for static parallelization of single-pass array-processing programs. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, 18\u201323 June 2017, pp. 572\u2013585. ACM (2017)","DOI":"10.1145\/3062341.3062382"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., R\u00fcmmer, P.: Competition report: CHC-COMP-21. In: Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2021, Virtual, EPTCS, 28 March 2021, vol. 344, pp. 91\u2013108 (2021)","DOI":"10.4204\/EPTCS.344.7"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Garoche, P., Kahsai, T., Thirioux, X.: Hierarchical state machines as modular horn clauses. In: Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, EPTCS, Eindhoven, The Netherlands, 3 April 2016, vol. 219, pp. 15\u201328 (2016)","DOI":"10.4204\/EPTCS.219.2"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, Beijing, China, 11\u201316 June 2012, pp. 405\u2013416. ACM (2012)","DOI":"10.1145\/2345156.2254112"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Bj\u00f8rner, N.: The science, art, and magic of constrained Horn clauses. In: 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2019, Timisoara, Romania, 4\u20137 September 2019, pp. 6\u201310. IEEE (2019)","DOI":"10.1109\/SYNASC49474.2019.00010"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-642-22110-1_36","volume-title":"Computer Aided Verification","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Bj\u00f8rner, N., de Moura, L.: $${\\mu }Z$$\u2013 an efficient engine for fixed points with constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 457\u2013462. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_36"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-32759-9_21","volume-title":"FM 2012: Formal Methods","author":"H Hojjat","year":"2012","unstructured":"Hojjat, H., Kone\u010dn\u00fd, F., Garnier, F., Iosif, R., Kuncak, V., R\u00fcmmer, P.: A verification toolkit for numerical transition systems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 247\u2013251. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_21"},{"issue":"20","key":"13_CR26","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19","author":"J Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. J. Log. Program. 19(20), 503\u2013581 (1994)","journal-title":"J. Log. Program."},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-319-41528-4_19","volume-title":"Computer Aided Verification","author":"T Kahsai","year":"2016","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: a framework for verifying Java programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 352\u2013358. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19"},{"key":"13_CR28","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus, Notes Series NS-01-1, January 2001. http:\/\/www.brics.dk\/mona\/"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, 4\u20138 June 2011, pp. 222\u2013233. ACM (2011)","DOI":"10.1145\/1993316.1993525"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"L\u00f6ding, C., Madhusudan, P., Pe\u00f1a, L.: Foundations for natural proofs and quantifier instantiation. Proc. ACM Program. Lang. 2(POPL), 10:1\u201310:30 (2018)","DOI":"10.1145\/3158098"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 January 2011, pp. 283\u2013294. ACM (2011)","DOI":"10.1145\/1925844.1926419"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 January 2011, pp. 611\u2013622. ACM (2011)","DOI":"10.1145\/1925844.1926455"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Qiu, X., Stefanescu, A.: Recursive proofs for inductive tree data-structures. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, 22\u201328 January 2012, pp. 123\u2013136. ACM (2012)","DOI":"10.1145\/2103621.2103673"},{"key":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-540-40007-3_24","volume-title":"Formal Methods at the Crossroads. From Panacea to Foundational Support","author":"Z Manna","year":"2003","unstructured":"Manna, Z., Zarba, C.G.: Combining decision procedures. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 381\u2013422. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-40007-3_24"},{"key":"13_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-030-44914-8_18","volume-title":"Programming Languages and Systems","author":"Y Matsushita","year":"2020","unstructured":"Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for rust programs. In: ESOP 2020. LNCS, vol. 12075, pp. 484\u2013514. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_18"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"13_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/11874683_3","volume-title":"Computer Science Logic","author":"L Segoufin","year":"2006","unstructured":"Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41\u201357. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11874683_3"},{"key":"13_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-030-88806-0_20","volume-title":"Static Analysis","author":"T Shimoda","year":"2021","unstructured":"Shimoda, T., Kobayashi, N., Sakayori, K., Sato, R.: Symbolic automatic relations and their applications to SMT and CHC solving. In: Dr\u0103goi, C., Mukherjee, S., Namjoshi, K. (eds.) SAS 2021. LNCS, vol. 12913, pp. 405\u2013428. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_20"},{"issue":"1","key":"13_CR39","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"JW Thatcher","year":"1968","unstructured":"Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Syst. Theory 2(1), 57\u201381 (1968)","journal-title":"Math. Syst. Theory"},{"key":"13_CR40","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: Van Leeuwen, J. (ed.) Formal Models and Semantics. In: Handbook of Theoretical Computer Science, pp. 133\u2013191. Elsevier, Amsterdam (1990)","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"13_CR41","unstructured":"Trakhtenbrot, B.A.: Finite automata and logic of monadic predicates. Doklady Akademii Nauk SSSR 149, 326\u2013329 (1961). (in Russian)"},{"issue":"3","key":"13_CR42","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1016\/j.ipl.2014.11.005","volume":"115","author":"M Veanes","year":"2015","unstructured":"Veanes, M., Bj\u00f8rner, N.: Symbolic tree automata. Inf. Process. Lett. 115(3), 418\u2013424 (2015)","journal-title":"Inf. Process. Lett."},{"key":"13_CR43","doi-asserted-by":"crossref","unstructured":"Veanes, M., de Halleux, P., Tillmann, N.: Rex: symbolic regular expression explorer. In: 2010 Third International Conference on Software Testing, Verification and Validation, pp. 498\u2013507 (2010)","DOI":"10.1109\/ICST.2010.15"}],"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-13188-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T17:05:59Z","timestamp":1659719159000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","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":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","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":"209","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":"40","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":"11","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":"19% - 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.9","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":"9.7","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)"}}]}}