{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:27:02Z","timestamp":1745994422672,"version":"3.40.3"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031787089"},{"type":"electronic","value":"9783031787096"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-78709-6_7","type":"book-chapter","created":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T22:10:28Z","timestamp":1738361428000},"page":"135-159","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Proving Cutoff Bounds for Safety Properties in First-Order Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-5883-5082","authenticated-orcid":false,"given":"Raz","family":"Lotan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4589-2173","authenticated-orcid":false,"given":"Eden","family":"Frenkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,2,1]]},"reference":[{"issue":"5","key":"7_CR1","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s10009-015-0406-x","volume":"18","author":"P Abdulla","year":"2015","unstructured":"Abdulla, P., Haziza, F., Hol\u00edk, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transfer 18(5), 495\u2013516 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0406-x","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Ashmore, R., Gurfinkel, A., Trefler, R.J.: Local reasoning for parameterized first order protocols. In: NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11460, pp. 36\u201353. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_3","DOI":"10.1007\/978-3-030-20652-9_3"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-662-49122-5_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Au\u00dferlechner","year":"2016","unstructured":"Au\u00dferlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 476\u2013494. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_23"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Ball, T., Bj\u00f8rner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: Vericon: towards verifying controller programs in software-defined networks. SIGPLAN Not. 49(6), 282\u2013293 (jun 2014). https:\/\/doi.org\/10.1145\/2666356.2594317","DOI":"10.1145\/2666356.2594317"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Bhat, S.G., Nagar, K.: Automating cutoff-based verification of distributed protocols. In: 2023 Formal Methods in Computer-Aided Design (FMCAD), pp. 75\u201385 (2023). https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_15","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_15"},{"key":"7_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1007\/978-3-030-81688-9_42","volume-title":"Computer Aided Verification","author":"S Chakraborty","year":"2021","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Diffy: inductive reasoning of array programs using difference invariants. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 911\u2013935. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_42"},{"issue":"5","key":"7_CR7","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1007\/S10009-022-00676-W","volume":"24","author":"S Chakraborty","year":"2022","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Full-program induction: verifying array programs sans loop invariants. Int. J. Softw. Tools Technol. Transf. 24(5), 843\u2013888 (2022). https:\/\/doi.org\/10.1007\/S10009-022-00676-W","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state- processes. In: Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing, pp. 240-248. PODC \u201986, Association for Computing Machinery, New York, NY, USA (1986). https:\/\/doi.org\/10.1145\/10590.10611","DOI":"10.1145\/10590.10611"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Elad, N., Padon, O., Shoham, S.: An infinite needle in a finite haystack: Finding infinite counter-models in deductive verification. Proc. ACM Program. Lang. 8(POPL) (jan 2024). https:\/\/doi.org\/10.1145\/3632875","DOI":"10.1145\/3632875"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings. Lecture Notes in Computer Science, vol.\u00a01831, pp. 236\u2013254. Springer (2000). https:\/\/doi.org\/10.1007\/10721959_19","DOI":"10.1007\/10721959_19"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 85\u201394. POPL \u201995, Association for Computing Machinery, New York, NY, USA (1995). https:\/\/doi.org\/10.1145\/199448.199468","DOI":"10.1145\/199448.199468"},{"key":"7_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/11888116_26","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"Y Fang","year":"2006","unstructured":"Fang, Y., McMillan, K.L., Pnueli, A., Zuck, L.D.: Liveness by Invisible Invariants. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 356\u2013371. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11888116_26"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proofs that count. SIGPLAN Not. 49(1), 151\u2013164 (jan 2014). https:\/\/doi.org\/10.1145\/2578855.2535885","DOI":"10.1145\/2578855.2535885"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Farzan, A., Klumpp, D., Podelski, A.: Commutativity simplifies proofs of parameterized programs. Proc. ACM Program. Lang. 8(POPL) (jan 2024). https:\/\/doi.org\/10.1145\/3632925","DOI":"10.1145\/3632925"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Feldman, Y.M.Y., Wilcox, J.R., Shoham, S., Sagiv, M.: Inferring inductive invariants from phase structures. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification. pp. 405\u2013425. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_23","DOI":"10.1007\/978-3-030-25543-5_23"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Shoham, S., Meshman, Y.: SMT-based verification of parameterized systems. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 338\u2013348. FSE 2016, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2950290.2950330","DOI":"10.1145\/2950290.2950330"},{"key":"7_CR17","unstructured":"Hance, T., Heule, M., Martins, R., Parno, B.: Finding invariants of distributed systems: It\u2019s a small (enough) world after all. In: 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21), pp. 115\u2013131. USENIX Association (Apr 2021). https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: a pearl in compositional verification. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 473\u2013485. POPL \u201917, Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3009837.3009893","DOI":"10.1145\/3009837.3009893"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Ish-Shalom, O., Itzhaky, S., Rinetzky, N., Shoham, S.: Putting the squeeze on array programs: Loop verification via inductive rank reduction. In: Verification, Model Checking, and Abstract Interpretation, pp. 112\u2013135. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-_6","DOI":"10.1007\/978-3-030-39322-_6"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Lahav, O., Nanevski, A., Sagiv, M.: Modular reasoning about heap paths via effectively propositional formulas. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014, pp. 385\u2013396. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535854","DOI":"10.1145\/2535838.2535854"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Jaber, N., Wagner, C., Jacobs, S., Kulkarni, M., Samanta, R.: Quicksilver: modeling and parameterized verification for distributed agreement-based systems. Proc. ACM Program. Lang. 5(OOPSLA) (oct 2021). https:\/\/doi.org\/10.1145\/3485534","DOI":"10.1145\/3485534"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Sakr, M.: Analyzing guarded protocols: Better cutoffs, more systems, more expressivity. In: Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10747, pp. 247\u2013268. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_12","DOI":"10.1007\/978-3-319-73721-8_12"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06174, pp. 645\u2013659. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_55","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Karbyshev, A., Bj\u00f8rner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. J. ACM 64(1) (mar 2017). https:\/\/doi.org\/10.1145\/3022187","DOI":"10.1145\/3022187"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Koenig, J.R., Padon, O., Shoham, S., Aiken, A.: Inferring invariants with quantifier alternations: Taming the search space explosion. In: Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13243, pp. 338\u2013356. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_18","DOI":"10.1007\/978-3-030-99524-9_18"},{"key":"7_CR26","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.12664114","author":"R Lotan","year":"2024","unstructured":"Lotan, R., Frenkel, E., Shoham, S.: Proving cutoff bounds for safety-properties in first-order logic (artifact). Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.12664114","journal-title":"Zenodo"},{"key":"7_CR27","unstructured":"Lotan, R., Frenkel, E., Shoham, S.: Proving cutoff bounds for safety properties in first-order logic (full version) (2024). https:\/\/arxiv.org\/abs\/2408.10685"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Maric, O., Sprenger, C., Basin, D.A.: Cutoff bounds for consensus algorithms. In: Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10427, pp. 217\u2013237. Springer (2017).https:\/\/doi.org\/10.1007\/978-3-319-63390-9_12","DOI":"10.1007\/978-3-319-63390-9_12"},{"key":"7_CR29","series-title":"LNCS","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"},{"issue":"OOPSLA2","key":"7_CR30","doi-asserted-by":"publisher","first-page":"1873","DOI":"10.1145\/3563354","volume":"6","author":"A Murali","year":"2022","unstructured":"Murali, A., Pe\u00f1a, L., Blanchard, E., L\u00f6ding, C., Madhusudan, P.: Model-guided synthesis of inductive lemmas for FOL with least fixpoints. Proc. ACM Program. Lang. 6(OOPSLA2), 1873\u20131902 (2022). https:\/\/doi.org\/10.1145\/3563354","journal-title":"Proc. ACM Program. Lang."},{"key":"7_CR31","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-69738-1_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KS Namjoshi","year":"2007","unstructured":"Namjoshi, K.S.: Symmetry and completeness in the analysis of parameterized systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 299\u2013313. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_22"},{"key":"7_CR32","unstructured":"Padon, O.: Deductive Verification of Distributed Protocols in First-Order Logic. Ph.D. thesis, Tel Aviv University, Israel (2018). https:\/\/tau.primo.exlibrisgroup.com\/permalink\/972TAU_INST\/bai57q\/alma9932991300004146"},{"key":"7_CR33","doi-asserted-by":"publisher","unstructured":"Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made epr: decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA) (oct 2017). https:\/\/doi.org\/10.1145\/3140568","DOI":"10.1145\/3140568"},{"key":"7_CR34","doi-asserted-by":"publisher","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: Safety verification by interactive generalization. In: PLDI \u201916: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 614\u2013630 (Jun 2016). https:\/\/doi.org\/10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Padon, O., Wilcox, J.R., Koenig, J.R., McMillan, K.L., Aiken, A.: Induction duality: primal-dual search for invariants. Proc. ACM Program. Lang. 6(POPL) (jan 2022). https:\/\/doi.org\/10.1145\/3498712","DOI":"10.1145\/3498712"},{"key":"7_CR36","doi-asserted-by":"publisher","unstructured":"Pani, T., Weissenbacher, G., Zuleger, F.: Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification. Formal Methods in System Design, pp. 1\u201338 (10 2023). https:\/\/doi.org\/10.1007\/s10703-023-00439-6","DOI":"10.1007\/s10703-023-00439-6"},{"key":"7_CR37","doi-asserted-by":"publisher","unstructured":"Ramsey, F.P.: On a Problem of Formal Logic, pp. 1\u201324. Birkh\u00e4user Boston, Boston, MA (1987). https:\/\/doi.org\/10.1007\/978-0-8176-4842-8_1","DOI":"10.1007\/978-0-8176-4842-8_1"},{"key":"7_CR38","doi-asserted-by":"publisher","unstructured":"Segall, A.: Distributed network protocols. IEEE Transactions on Information Theory 29(1), 23\u201335 (1983). https:\/\/doi.org\/10.1109\/TIT.1983.1056620","DOI":"10.1109\/TIT.1983.1056620"},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"Tamir, O., Taube, M., McMillan, K.L., Shoham, S., Howell, J., Gueta, G., Sagiv, M.: Counterexample driven quantifier instantiations with applications to distributed protocols. Proc. ACM Program. Lang. 7(OOPSLA2) (oct 2023). https:\/\/doi.org\/10.1145\/3622864","DOI":"10.1145\/3622864"},{"key":"7_CR40","doi-asserted-by":"publisher","unstructured":"Taube, M., et al.: Modularity for decidability of deductive verification with applications to distributed systems. SIGPLAN Not. 53(4), 662\u2013677 (jun 2018). https:\/\/doi.org\/10.1145\/3296979.3192414","DOI":"10.1145\/3296979.3192414"},{"key":"7_CR41","doi-asserted-by":"publisher","unstructured":"Tran, T., Konnov, I., Widder, J.: Cutoffs for symmetric point-to-point distributed algorithms. In: Networked Systems - 8th International Conference, NETYS 2020, Marrakech, Morocco, June 3-5, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12129, pp. 329\u2013346. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-67087-0_21","DOI":"10.1007\/978-3-030-67087-0_21"},{"key":"7_CR42","doi-asserted-by":"publisher","unstructured":"Wagner, C., Jaber, N., Samanta, R.: Enabling bounded verification of doubly-unbounded distributed agreement-based systems via bounded regions. Proc. ACM Program. Lang. 7(OOPSLA1) (2023). https:\/\/doi.org\/10.1145\/3586033","DOI":"10.1145\/3586033"},{"key":"7_CR43","doi-asserted-by":"publisher","unstructured":"Wilcox, J.R., Feldman, Y.M.Y., Padon, O., Shoham, S.: mypyvy: A research platform for verification of transition systems in first-order logic. In: Computer Aided Verification, pp. 71\u201385. Springer Nature Switzerland, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_4","DOI":"10.1007\/978-3-031-65630-9_4"},{"key":"7_CR44","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J.: DuoAI: Fast, automated inference of inductive invariants for verifying distributed protocols. In: 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22), pp. 485\u2013501. USENIX Association, Carlsbad, CA (Jul 2022). https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/yao"},{"key":"7_CR45","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J., Jana, S., Ryan, G.: DistAI: data-driven automated invariant learning for distributed protocols. In: 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21), pp. 405\u2013421. USENIX Association (Jul 2021). https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78709-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T22:10:55Z","timestamp":1738361455000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78709-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031787089","9783031787096"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78709-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 February 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}