{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T23:47:35Z","timestamp":1769730455773,"version":"3.49.0"},"publisher-location":"Cham","reference-count":47,"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>Satisfiability Modulo Linear Integer Arithmetic, SMT (LIA) for short, has significant applications in many domains. In this paper, we develop the first local search algorithm for SMT (LIA) by directly operating on variables, breaking through the traditional framework. We propose a local search framework by considering the distinctions between Boolean and integer variables. Moreover, we design a novel operator and scoring functions tailored for LIA, and propose a two-level operation selection heuristic. Putting these together, we develop a local search SMT (LIA) solver called LS-LIA. Experiments are carried out to evaluate LS-LIA on benchmarks from SMTLIB and two benchmark sets generated from job shop scheduling and data race detection. The results show that LS-LIA is competitive and complementary with state-of-the-art SMT solvers, and performs particularly well on those formulae with only integer variables. A simple sequential portfolio with Z3 improves the state-of-the-art on satisfiable benchmark sets of LIA and IDL benchmarks from SMT-LIB. LS-LIA also solves Job Shop Scheduling benchmarks substantially faster than traditional complete SMT solvers.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_12","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"227-248","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Local Search for\u00a0SMT on\u00a0Linear Integer Arithmetic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1730-6922","authenticated-orcid":false,"given":"Shaowei","family":"Cai","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1356-6057","authenticated-orcid":false,"given":"Bohan","family":"Li","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5541-7194","authenticated-orcid":false,"given":"Xindi","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-31612-8_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Balint","year":"2012","unstructured":"Balint, A., Sch\u00f6ning, U.: Choosing probability distributions for stochastic local search and the role of make versus break. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 16\u201329. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_3"},{"key":"12_CR2","unstructured":"Barrett, C., Barbosa, H., Brain, M., et al.: Cvc5 at the SMT competition 2021 (2021)"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"12_CR4","first-page":"44","volume":"2016","author":"A Biere","year":"2016","unstructured":"Biere, A.: Splatz, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT competition 2016. Proc. SAT Competition 2016, 44\u201345 (2016)","journal-title":"Proc. SAT Competition"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Blackburn, S.M., Garner, R., Hoffmann, C., et al.: The DaCapo benchmarks: Java benchmarking development and analysis, pp. 169\u2013190 (2006)","DOI":"10.1145\/1167515.1167488"},{"key":"12_CR6","unstructured":"Bromberger, M.: Decision procedures for linear arithmetic. Ph.D. thesis, Saarland University, Saarbr\u00fccken, Germany (2019)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-030-29436-6_7","volume-title":"Automated Deduction \u2013 CADE 27","author":"M Bromberger","year":"2019","unstructured":"Bromberger, M., Fleury, M., Schwarz, S., Weidenbach, C.: SPASS-SATT. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 111\u2013122. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_7"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-319-40229-1_9","volume-title":"Automated Reasoning","author":"M Bromberger","year":"2016","unstructured":"Bromberger, M., Weidenbach, C.: Fast cube tests for LIA constraint solving. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 116\u2013132. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_9"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"RE Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78\u201392. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_7"},{"key":"12_CR10","unstructured":"Cai, S.: Balance between complexity and quality: local search for minimum vertex cover in massive graphs. In: Proceedings of IJCAI 2015, pp. 747\u2013753 (2015)"},{"key":"12_CR11","unstructured":"Cai, S., Li, B., Zhang, X.: YicesLS on SMT COMP2021 (2021)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-24318-4_1","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"S Cai","year":"2015","unstructured":"Cai, S., Luo, C., Su, K.: CCAnr: a configuration checking based local search solver for non-random satisfiability. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 1\u20138. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_1"},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.artint.2013.09.001","volume":"204","author":"S Cai","year":"2013","unstructured":"Cai, S., Su, K.: Local search for Boolean satisfiability with configuration checking and subscore. Artif. Intell. 204, 75\u201398 (2013)","journal-title":"Artif. Intell."},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Model Checking Software","author":"J Christ","year":"2012","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248\u2013254. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31759-0_19"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Codish, M., Fekete, Y., Fuhs, C., Giesl, J., Waldmann, J.: Exotic semi-ring constraints. In: SMT@ IJCAR 20, pp. 88\u201397 (2012)","DOI":"10.29007\/qqvt"},{"key":"12_CR17","unstructured":"Cotton, S., Podelski, A., Finkbeiner, B.: Satisfiability checking with difference constraints. IMPRS Computer Science, Saarbruceken (2005)"},{"key":"12_CR18","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":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_11"},{"key":"12_CR20","unstructured":"Dutertre, B., De Moura, L.: Integrating simplex with DPLL (T). Computer Science Laboratory, SRI International, Technical Report SRI-CSL-06-01 (2006)"},{"key":"12_CR21","unstructured":"Dutertre, B., De Moura, L.: The YICES SMT solver, vol. 2, no. 2, pp. 1\u20132 (2006). Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Fr\u00f6hlich, A., Biere, A., Wintersteiger, C., Hamadi, Y.: Stochastic local search for satisfiability modulo theories. In: Proceedings of AAAI 2015, vol. 29 (2015)","DOI":"10.1609\/aaai.v29i1.9372"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/11691372_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MK Ganai","year":"2006","unstructured":"Ganai, M.K., Talupur, M., Gupta, A.: SDSAT: tight integration of small domain encoding and lazy approaches in a separation logic solver. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 135\u2013150. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_9"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Gavrilenko, N., Ponce-de-Le\u00f3n, H., Furbach, F., Heljanko, K., Meyer, R.: BMC for weak memory models: relation analysis for compact SMT encodings. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 355\u2013365. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_19","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Glover, F., Laguna, M.: Tabu search. In: Du, D.Z., Pardalos, P.M. (eds.) Handbook of Combinatorial Optimization. Springer, Boston (1998). https:\/\/doi.org\/10.1007\/978-1-4613-0303-9_33","DOI":"10.1007\/978-1-4613-0303-9_33"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-24364-6_12","volume-title":"Frontiers of Combining Systems","author":"A Griggio","year":"2011","unstructured":"Griggio, A., Phan, Q.-S., Sebastiani, R., Tomasi, S.: Stochastic local search for SMT: combining theory solvers with walkSAT. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 163\u2013178. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24364-6_12"},{"key":"12_CR27","unstructured":"Hentenryck, P.V., Michel, L.: Constraint-based local search (2009)"},{"key":"12_CR28","unstructured":"Hoos, H.H., St\u00fctzle, T.: Stochastic local search: foundations and applications (2004)"},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Huang, J., Meredith, P.O., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. In: Proceedings of PLDI 2014, pp. 337\u2013348 (2014)","DOI":"10.1145\/2666356.2594315"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-04238-6_14","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"T Janhunen","year":"2009","unstructured":"Janhunen, T., Niemel\u00e4, I., Sevalnev, M.: Computing stable models via reductions to difference logic. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS (LNAI), vol. 5753, pp. 142\u2013154. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04238-6_14"},{"issue":"1\u20132","key":"12_CR31","first-page":"47","volume":"3","author":"H Kim","year":"2007","unstructured":"Kim, H., Jin, H., Somenzi, F.: Disequality management in integer difference logic via finite instantiations. JSAT 3(1\u20132), 47\u201366 (2007)","journal-title":"JSAT"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"King, T., Barrett, C., Dutertre, B.: Simplex with sum of infeasibilities for SMT. In: Proceedings of FMCAD 2013, pp. 189\u2013196 (2013)","DOI":"10.1109\/FMCAD.2013.6679409"},{"key":"12_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-31612-8_43","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"CM Li","year":"2012","unstructured":"Li, C.M., Li, Y.: Satisfying versus falsifying in local search for satisfiability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 477\u2013478. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_43"},{"issue":"4","key":"12_CR34","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/s10009-015-0366-1","volume":"18","author":"NP Lopes","year":"2015","unstructured":"Lopes, N.P., Monteiro, J.: Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. Int. J. Softw. Tools Technol. Transfer 18(4), 359\u2013374 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0366-1","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds) Program Verification. Studies in Cognitive Systems, vol 14. Springer, Dordrecht. https:\/\/doi.org\/10.1007\/978-94-011-1793-7_2","DOI":"10.1007\/978-94-011-1793-7_2"},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-319-41528-4_11","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2016","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Precise and complete propagation based local search for satisfiability modulo theories. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 199\u2013217. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_11"},{"key":"12_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321\u2013334. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_33"},{"issue":"6","key":"12_CR38","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"1","key":"12_CR39","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0890-5401(02)93175-5","volume":"178","author":"A Pnueli","year":"2002","unstructured":"Pnueli, A., Rodeh, Y., Strichman, O., Siegel, M.: The small model property: how small can it be? Inf. Comput. 178(1), 279\u2013293 (2002)","journal-title":"Inf. Comput."},{"key":"12_CR40","doi-asserted-by":"crossref","unstructured":"Roselli, S.F., Bengtsson, K., \u00c5kesson, K.: SMT solvers for job-shop scheduling problems: models comparison and performance evaluation. In: Proceedings of CASE 2018, pp. 547\u2013552 (2018)","DOI":"10.1109\/COASE.2018.8560344"},{"issue":"3\u20134","key":"12_CR41","first-page":"141","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. JSAT 3(3\u20134), 141\u2013224 (2007)","journal-title":"JSAT"},{"key":"12_CR42","doi-asserted-by":"crossref","unstructured":"Selman, B., Kautz, H.A., Cohen, B., et al.: Local search strategies for satisfiability testing. In: Cliques, Coloring, and Satisfiability, vol. 26, pp. 521\u2013532 (1993)","DOI":"10.1090\/dimacs\/026\/25"},{"key":"12_CR43","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Proceedings of DAC 2003, pp. 425\u2013430 (2003)","DOI":"10.1145\/775832.775945"},{"key":"12_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45657-0_16","volume-title":"Computer Aided Verification","author":"O Strichman","year":"2002","unstructured":"Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 209\u2013222. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_16"},{"key":"12_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-27813-9_12","volume-title":"Computer Aided Verification","author":"M Talupur","year":"2004","unstructured":"Talupur, M., Sinha, N., Strichman, O., Pnueli, A.: Range allocation for separation logic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 148\u2013161. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_12"},{"key":"12_CR46","unstructured":"Thornton, J., Pham, D.N., Bain, S., Ferreira, V., Jr.: Additive versus multiplicative clause weighting for SAT. In: Proceedings of AAAI 2004, pp. 191\u2013196 (2004)"},{"key":"12_CR47","doi-asserted-by":"crossref","unstructured":"Wang, C., Gupta, A., Ganai, M.: Predicate learning and selective theory deduction for a difference logic solver. In: Proceedings of DAC 2006, pp. 235\u2013240 (2006)","DOI":"10.1145\/1146909.1146971"}],"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_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,30]],"date-time":"2024-09-30T20:21:56Z","timestamp":1727727716000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_12","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)"}}]}}