{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T13:01:43Z","timestamp":1760101303282,"version":"3.40.3"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720155"},{"type":"electronic","value":"9783030720162"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction refinement scheme for the theory of arrays. Our framework can thus, in many cases, reduce inductive reasoning with quantifiers and arrays to quantifier-free and array-free reasoning. We evaluate the approach on a wide set of benchmarks from the literature. The results show that our implementation often outperforms state-of-the-art tools, demonstrating its practical potential.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_7","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"113-132","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1555-5784","authenticated-orcid":false,"given":"Makai","family":"Mann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7791-9021","authenticated-orcid":false,"given":"Ahmed","family":"Irfan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3311-0893","authenticated-orcid":false,"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[]},{"given":"Oded","family":"Padon","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. In: Proceedings of the 3rd Annual Symposium on Logic in Computer Science. pp. 165\u2013175 (July 1988), https:\/\/www.microsoft.com\/en-us\/research\/publication\/the-existence-of-refinement-mappings\/, lICS 1988 Test of Time Award","key":"7_CR1"},{"doi-asserted-by":"crossref","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: smt-based abstraction for arrays with interpolants. In: CAV. Lecture Notes in Computer Science, vol. 7358, pp. 679\u2013685. Springer (2012)","key":"7_CR2","DOI":"10.1007\/978-3-642-31424-7_49"},{"doi-asserted-by":"crossref","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Booster: An acceleration-based verification framework for array programs. In: ATVA. Lecture Notes in Computer Science, vol. 8837, pp. 18\u201323. Springer (2014)","key":"7_CR3","DOI":"10.1007\/978-3-319-11936-6_2"},{"unstructured":"Alur, R., Bod\u00edk, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 40, pp. 1\u201325. IOS Press (2015)","key":"7_CR4"},{"doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proceedings of the 23rd International Conference on Computer Aided Verification (CAV \u201911). Lecture Notes in Computer Science, vol. 6806, pp. 171\u2013177. Springer (Jul 2011), http:\/\/www.cs.stanford.edu\/~barrett\/pubs\/BCD+11.pdf, snowbird, Utah","key":"7_CR5","DOI":"10.1007\/978-3-642-22110-1_14"},{"unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)","key":"7_CR6"},{"doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer (2018)","key":"7_CR7","DOI":"10.1007\/978-3-319-10575-8_11"},{"doi-asserted-by":"crossref","unstructured":"Beyer, D.: Software verification with validation of results - (report on SV-COMP 2017). In: TACAS (2). Lecture Notes in Computer Science, vol. 10206, pp. 331\u2013349 (2017)","key":"7_CR8","DOI":"10.1007\/978-3-662-54580-5_20"},{"doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 193\u2013207. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)","key":"7_CR9","DOI":"10.1007\/3-540-49059-0_14"},{"doi-asserted-by":"publisher","unstructured":"Bjesse, P.: Word-level sequential memory abstraction for model checking. In: 2008 Formal Methods in Computer Aided Design. pp. 1\u20139 (Nov 2008). https:\/\/doi.org\/10.1109\/FMCAD.2008.ECP.20","key":"7_CR10","DOI":"10.1109\/FMCAD.2008.ECP.20"},{"doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Fields of Logic and Computation II. Lecture Notes in Computer Science, vol. 9300, pp. 24\u201351. Springer (2015)","key":"7_CR11","DOI":"10.1007\/978-3-319-23534-9_2"},{"doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: Sat-based model checking without unrolling. In: VMCAI. Lecture Notes in Computer Science, vol. 6538, pp. 70\u201387. Springer (2011)","key":"7_CR12","DOI":"10.1007\/978-3-642-18275-4_7"},{"doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 427\u2013442. Springer Berlin Heidelberg, Berlin,Heidelberg (2006)","key":"7_CR13","DOI":"10.1007\/11609773_28"},{"doi-asserted-by":"publisher","unstructured":"Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. In: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning. p. 6\u201311. SMT \u201908\/BPR \u201908, Association for Computing Machinery, New York, NY, USA (2008). https:\/\/doi.org\/10.1145\/1512464.1512467, https:\/\/doi.org\/10.1145\/1512464.1512467","key":"7_CR14","DOI":"10.1145\/1512464.1512467"},{"unstructured":"Bueno, D., Cox, A., Sakallah, K.: Euficient reachability for software with arrays. In: Formal Methods in Computer Aided Design (2020)","key":"7_CR15"},{"unstructured":"Chen, Y., Kov\u00e1cs, L., Robillard, S.: Theory-specific reasoning about loops with arrays using vampire. In: Vampire@IJCAR. EPiC Series in Computing, vol. 44, pp. 16\u201332. EasyChair (2016)","key":"7_CR16"},{"doi-asserted-by":"crossref","unstructured":"Christ, J., Hoenicke, J.: Weakly equivalent arrays. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems. pp. 119\u2013134. Springer International Publishing, Cham (2015)","key":"7_CR17","DOI":"10.1007\/978-3-319-24246-0_8"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. 19(3), 19:1\u201319:52 (2018)","key":"7_CR18","DOI":"10.1145\/3230639"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos - A software model checker for systemc. In: CAV. Lecture Notes in Computer Science, vol. 6806, pp. 310\u2013316. Springer (2011)","key":"7_CR19","DOI":"10.1007\/978-3-642-22110-1_24"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods in System Design 49(3), 190\u2013218 (2016)","key":"7_CR20","DOI":"10.1007\/s10703-016-0257-4"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S. (eds.) Proceedings of TACAS. LNCS, vol. 7795. Springer (2013)","key":"7_CR21","DOI":"10.1007\/978-3-642-36742-7_7"},{"unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif. Intell. Res. 40, 701\u2013728 (2011)","key":"7_CR22"},{"unstructured":"Cimatti, A., Roveri, M., Griggio, A., Irfan, A.: Verification Modulo Theories. http:\/\/www.vmt-lib.org (2011)","key":"7_CR23"},{"unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. Formal Methods Syst. Des. 34(2), 104\u2013125 (2009)","key":"7_CR24"},{"doi-asserted-by":"crossref","unstructured":"Conchon, S., Goel, A., Krstic, S., Majumdar, R., Roux, M.: Far-cubicle - A new reachability algorithm for cubicle. In: FMCAD. pp. 172\u2013175. IEEE (2017)","key":"7_CR25","DOI":"10.23919\/FMCAD.2017.8102256"},{"unstructured":"Craig, W.: Linear reasoning. A new form of the herbrand-gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957)","key":"7_CR26"},{"doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: 2009 Formal Methods in Computer-Aided Design. pp. 45\u201352 (Nov 2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351142","key":"7_CR27","DOI":"10.1109\/FMCAD.2009.5351142"},{"unstructured":"Fedyukovich, G.: Freqhorn implementation, https:\/\/github.com\/grigoryfedyukovich\/aeval\/commit\/f5cc11808c1b73886a4e7d5a71daeffb45470b9a","key":"7_CR28"},{"doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: CAV (1). Lecture Notes in Computer Science, vol. 11561, pp. 259\u2013277. Springer (2019)","key":"7_CR29","DOI":"10.1007\/978-3-030-25540-4_14"},{"unstructured":"Georgiou, P., Gleiss, B., Kov\u00e1cs, L.: Trace logic for inductive loop reasoning. In: Formal Methods in Computer Aided Design (2020)","key":"7_CR30"},{"doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: MCMT: A model checker modulo theories. In: Giesl, J., H\u00e4hnle, R. (eds.) Automated Reasoning. pp. 22\u201329. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)","key":"7_CR31","DOI":"10.1007\/978-3-642-14203-1_3"},{"doi-asserted-by":"publisher","unstructured":"Goel, A., Krsti\u0107, S., Fuchs, A.: Deciding array formulas with frugal axiom instantiation. In: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning. p. 12\u201317. SMT \u201908\/BPR \u201908, Association for Computing Machinery, New York, NY, USA (2008). https:\/\/doi.org\/10.1145\/1512464.1512468, https:\/\/doi.org\/10.1145\/1512464.1512468","key":"7_CR32","DOI":"10.1145\/1512464.1512468"},{"unstructured":"Goel, A., Krstic, S., Leslie, R., Tuttle, M.R.: Smt-based system verification with DVF. In: SMT@IJCAR. EPiC Series in Computing, vol. 20, pp. 32\u201343. EasyChair (2012)","key":"7_CR33"},{"unstructured":"Griggio, A.: Open-source ic3 modulo theories with implicit predicate abstraction. https:\/\/es-static.fbk.eu\/people\/griggio\/ic3ia\/index.html (Accessed 2020), https:\/\/es-static.fbk.eu\/people\/griggio\/ic3ia\/index.html","key":"7_CR34"},{"doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: CAV (1). Lecture Notes in Computer Science, vol. 9206, pp. 343\u2013361. Springer (2015)","key":"7_CR35","DOI":"10.1007\/978-3-319-21690-4_20"},{"doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Shoham, S., Meshman, Y.: Smt-based verification of parameterized systems. In: SIGSOFT FSE. pp. 338\u2013348. ACM (2016)","key":"7_CR36","DOI":"10.1145\/2950290.2950330"},{"doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis. pp. 248\u2013266. Springer International Publishing, Cham (2018)","key":"7_CR37","DOI":"10.1007\/978-3-030-01090-4_15"},{"doi-asserted-by":"publisher","unstructured":"Hyberts, S.H., Jensen, P.G., Neele, T.: Tacas 21 artifact evaluation vm - ubuntu 20.04 lts (Sep 2020). https:\/\/doi.org\/10.5281\/zenodo.4041464","key":"7_CR38","DOI":"10.5281\/zenodo.4041464"},{"unstructured":"Kahsai, T., Kersten, R., R\u00fcmmer, P., Sch\u00e4f, M.: Quantified heap invariants for object-oriented programs. In: LPAR. EPiC Series in Computing, vol. 46, pp. 368\u2013384. EasyChair (2017)","key":"7_CR39"},{"doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. pp. 17\u201334. Springer International Publishing, Cham (2014)","key":"7_CR40","DOI":"10.1007\/978-3-319-08867-9_2"},{"doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: FASE. Lecture Notes in Computer Science, vol. 5503, pp. 470\u2013485. Springer (2009)","key":"7_CR41","DOI":"10.1007\/978-3-642-00593-0_33"},{"doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: CAV. Lecture Notes in Computer Science, vol. 8044, pp. 1\u201335. Springer (2013)","key":"7_CR42","DOI":"10.1007\/978-3-642-39799-8_1"},{"unstructured":"Krishnan, H.G.V., Gurfinkel, A.: Spacer CHC-COMP 2020 Submission (2020), https:\/\/www.starexec.org\/starexec\/secure\/details\/configuration.jsp?id=350966","key":"7_CR43"},{"doi-asserted-by":"crossref","unstructured":"Kroening, D., Groce, A., Clarke, E.M.: Counterexample guided abstraction refinement via program execution. In: ICFEM. Lecture Notes in Computer Science, vol. 3308, pp. 224\u2013238. Springer (2004)","key":"7_CR44","DOI":"10.1007\/978-3-540-30482-1_23"},{"doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: CAV. Lecture Notes in Computer Science, vol. 3114, pp. 135\u2013147. Springer (2004)","key":"7_CR45","DOI":"10.1007\/978-3-540-27813-9_11"},{"doi-asserted-by":"publisher","unstructured":"Li, B., Tang, Z., Zhai, J., Zhao, J.: Automatic invariant synthesis for arrays in simple programs. In: 2016 IEEE International Conference on Software Quality, Reliability and Security (QRS). pp. 108\u2013119 (Aug 2016). https:\/\/doi.org\/10.1109\/QRS.2016.23","key":"7_CR46","DOI":"10.1109\/QRS.2016.23"},{"doi-asserted-by":"crossref","unstructured":"Ma, H., Goel, A., Jeannin, J., Kapritsos, M., Kasikci, B., Sakallah, K.A.: I4: incremental inference of inductive invariants for verification of distributed protocols. In: SOSP. pp. 370\u2013384. ACM (2019)","key":"7_CR47","DOI":"10.1145\/3341301.3359651"},{"unstructured":"Mann, M., Irfan, A.: Prophic3 prototype, https:\/\/github.com\/makaimann\/prophic3\/commit\/497e2fbfb813bcf0a2c3bcb5b55ad47b2a678611","key":"7_CR48"},{"unstructured":"Mann, M., Irfan, A., Griggio, A., Padon, O., Barrett, C.: FigShare Artifact for Counterexample Guided Prophecy for Model Checking Modulo the Theory of Arrays, https:\/\/doi.org\/10.6084\/m9.figshare.13619096","key":"7_CR49"},{"unstructured":"Mccarthy, J.: Towards a mathematical science of computation. In: In IFIP Congress. pp. 21\u201328. North-Holland (1962)","key":"7_CR50"},{"doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 413\u2013427. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","key":"7_CR51","DOI":"10.1007\/978-3-540-78800-3_31"},{"doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Eager abstraction for symbolic model checking. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification. pp. 191\u2013208. Springer International Publishing, Cham (2018)","key":"7_CR52","DOI":"10.1007\/978-3-319-96145-3_11"},{"doi-asserted-by":"crossref","unstructured":"Monniaux, D., Gonnord, L.: Cell morphing: From array programs to array-free horn clauses. In: SAS. Lecture Notes in Computer Science, vol. 9837, pp. 361\u2013382. Springer (2016)","key":"7_CR53","DOI":"10.1007\/978-3-662-53413-7_18"},{"doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 337\u2013340. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","key":"7_CR54","DOI":"10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"publisher","unstructured":"Padon, O., Hoenicke, J., McMillan, K.L., Podelski, A., Sagiv, M., Shoham, S.: Temporal prophecy for proving temporal properties of infinite-state systems. In: 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. pp. 1\u201311 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603008, https:\/\/doi.org\/10.23919\/FMCAD.2018.8603008","key":"7_CR55","DOI":"10.23919\/FMCAD.2018.8603008"},{"unstructured":"Polgreen, E., Seshia, S.A.: Synrg: Syntax guided synthesis of invariants with alternating quantifiers. CoRR abs\/2007.10519 (2020)","key":"7_CR56"},{"unstructured":"R\u00fcmmer, P.: CHC COMP 2020. https:\/\/chc-comp.github.io\/ (2020)","key":"7_CR57"},{"unstructured":"R\u00fcmmer, P.: Competition Report: CHC-COMP-20 (2020), https:\/\/arxiv.org\/abs\/2008.02939","key":"7_CR58"},{"doi-asserted-by":"crossref","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a sat-solver. In: FMCAD. Lecture Notes in Computer Science, vol. 1954, pp. 108\u2013125. Springer (2000)","key":"7_CR59","DOI":"10.1007\/3-540-40922-X_8"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T00:06:58Z","timestamp":1616371618000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"141","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":"41","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":"21","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":"29% - 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":"12","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)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}