{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:37:53Z","timestamp":1781239073829,"version":"3.54.1"},"publisher-location":"Cham","reference-count":73,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816872","type":"print"},{"value":"9783030816889","type":"electronic"}],"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,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"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>Symbolic model checking is an important tool for finding bugs (or proving the absence of bugs) in modern system designs. Because of this, improving the ease of use, scalability, and performance of model checking tools and algorithms continues to be an important research direction. In service of this goal, we present , an open-source SMT-based model checker.  is designed to be both a research platform for developing and improving model checking algorithms, as well as a performance-competitive tool that can be used for academic and industry verification applications. In addition to performance,  prioritizes transparency (developed as an open-source project on GitHub), flexibility ( can be adapted to a variety of tasks by exploiting its general SMT-based interface), and extensibility (it is easy to add new algorithms and new back-end solvers). In this paper, we describe the design of the tool with a focus on the flexible and extensible architecture, cover its current capabilities, and demonstrate that  is competitive with state-of-the-art tools.<\/jats:p>","DOI":"10.1007\/978-3-030-81688-9_22","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:20:47Z","timestamp":1626452447000},"page":"461-474","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["Pono: A Flexible and Extensible SMT-Based Model Checker"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1555-5784","authenticated-orcid":false,"given":"Makai","family":"Mann","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7791-9021","authenticated-orcid":false,"given":"Ahmed","family":"Irfan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5715-7231","authenticated-orcid":false,"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yahan","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongce","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9374-9138","authenticated-orcid":false,"given":"Kristopher","family":"Brown","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6676-9400","authenticated-orcid":false,"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"22_CR1","unstructured":"AVR distribution. https:\/\/github.com\/aman-goel\/avr"},{"key":"22_CR2","unstructured":"btor2tools. https:\/\/github.com\/Boolector\/btor2tools"},{"key":"22_CR3","unstructured":"CMake. https:\/\/cmake.org"},{"key":"22_CR4","unstructured":"cosa2. https:\/\/github.com\/upscale-project\/cosa2"},{"key":"22_CR5","unstructured":"GoogleTest. https:\/\/github.com\/google\/googletest"},{"key":"22_CR6","unstructured":"Kind site. http:\/\/clc.cs.uiowa.edu\/Kind\/index.php?page=experimental-results"},{"key":"22_CR7","unstructured":"Pono. https:\/\/github.com\/upscale-project\/pono"},{"key":"22_CR8","unstructured":"ProphIC3 (commit: 497e2fbfb813bcf0a2c3bcb5b55ad47b2a678611). https:\/\/github.com\/makaimann\/prophic3"},{"key":"22_CR9","unstructured":"pytest 5.4.2. https:\/\/github.com\/pytest-dev\/pytest"},{"key":"22_CR10","unstructured":"IEEE Std 1364\u20132005, pp. 1\u2013590 (2006)"},{"key":"22_CR11","unstructured":"CoreIR (2017). https:\/\/github.com\/rdaly525\/coreir"},{"key":"22_CR12","unstructured":"Google Perftools (2017). https:\/\/github.com\/gperftools\/gperftools"},{"key":"22_CR13","unstructured":"ic3ia. https:\/\/es-static.fbk.eu\/people\/griggio\/ic3ia\/index.html. Accessed 2020"},{"key":"22_CR14","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. In: Proceedings of LICS, pp. 165\u2013175, July 1988"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Alberti, F., Bruttomesso, R., et al.: SAFARI: SMT-based abstraction for arrays with interpolants. In: Proceedings of CAV, pp. 679\u2013685 (2012)","DOI":"10.1007\/978-3-642-31424-7_49"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an acceleration-based verification framework for array programs. In: Proceedings of ATVA, pp. 18\u201323 (2014)","DOI":"10.1007\/978-3-319-11936-6_2"},{"key":"22_CR17","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.smt-lib.org"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., et al.: CVC4. In: Proceedings of CAV, pp. 171\u2013177 (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"22_CR19","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825\u2013885 (2009)"},{"key":"22_CR20","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/MCSE.2010.118","volume":"2","author":"S Behnel","year":"2011","unstructured":"Behnel, S., Bradshaw, R., Citro, C., Dalcin, L., Seljebotn, D.S., Smith, K.: Cython: the best of both worlds. Comput. Sci. Eng. 2, 31\u201339 (2011)","journal-title":"Comput. Sci. Eng."},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of TACAS, pp. 193\u2013207 (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"22_CR22","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition (2020). http:\/\/fmv.jku.at\/hwmcc20\/"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Birgmeier, J., Bradley, A., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Proceedings of CAV, pp. 831\u2013848 (2014)","DOI":"10.1007\/978-3-319-08867-9_55"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Gurfinkel, A.: Property directed polyhedral abstraction. In: Proceedings of VMCAI, pp. 263\u2013281 (2015)","DOI":"10.1007\/978-3-662-46081-8_15"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Bradley, A.: SAT-based model checking without unrolling. In: Proceedings of VMCAI, pp. 70\u201387 (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Brayton, R., Mishchenko, A.: ABC: An academic industrial-strength verification tool. In: Proceedings of CAV, pp. 24\u201340 (2010)","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"22_CR27","unstructured":"Bruttomesso, R.: Intrepid: An SMT-based model checker for control engineering and industrial automation. In: SMT Workshop, August 2019"},{"key":"22_CR28","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"8","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 8, 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Cartmell, J.: Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic 209\u2013243 (1986)","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"22_CR30","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., et al.: The nuXmv symbolic model checker. In: Proceedings of CAV, pp. 334\u2013342 (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Proceedings of CAV, pp. 510\u2013517 (2016)","DOI":"10.1007\/978-3-319-41540-6_29"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Proceedings of CAV, pp. 495\u2013499 (1999)","DOI":"10.1007\/3-540-48683-6_44"},{"key":"22_CR33","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Proceedings of CAV, pp. 359\u2013364 (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"22_CR34","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Irfan, A., et al.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. 19:1\u201319:52 (2018)","DOI":"10.1145\/3230639"},{"key":"22_CR35","first-page":"190","volume":"3","author":"A Cimatti","year":"2016","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant checking with IC3 and predicate abstraction. FMSD 3, 190\u2013218 (2016)","journal-title":"FMSD"},{"key":"22_CR36","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 (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"22_CR37","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. (1), 7:1\u20137:54 (2010)","DOI":"10.1145\/1838552.1838559"},{"key":"22_CR38","unstructured":"Cimatti, A., et al.: Verification Modulo Theories (2011). http:\/\/www.vmt-lib.org"},{"key":"22_CR39","doi-asserted-by":"crossref","unstructured":"Clarke, E., Henzinger, T., et al.: Handbook of Model Checking (2018)","DOI":"10.1007\/978-3-319-10575-8"},{"key":"22_CR40","doi-asserted-by":"crossref","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. (3), 250\u2013268 (1957)","DOI":"10.2307\/2963593"},{"key":"22_CR41","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Proceedings of CAV, pp. 737\u2013744 (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"22_CR42","doi-asserted-by":"crossref","unstructured":"Dutertre, B., Jovanovic, D., Navas, J.A.: Verification of fault-tolerant protocols with Sally. In: Proceedings of NFM, pp. 113\u2013120 (2018)","DOI":"10.1007\/978-3-319-77935-5_8"},{"key":"22_CR43","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Proceedings of FMCAD, pp. 125\u2013134 (2011)"},{"key":"22_CR44","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Proceedings of CAV, pp. 259\u2013277 (2019)","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"22_CR45","unstructured":"Gario, M., Micheli, A.: PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms. In: Proceedings of SMT Workshop, pp. 373\u2013384 (2015)"},{"key":"22_CR46","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Automated Reasoning, pp. 22\u201329 (2010)","DOI":"10.1007\/978-3-642-14203-1_3"},{"key":"22_CR47","doi-asserted-by":"crossref","unstructured":"Goel, A., Sakallah, K.A.: Model checking of Verilog RTL using IC3 with syntax-guided abstraction. In: Proceedings of NFM, pp. 166\u2013185 (2019)","DOI":"10.1007\/978-3-030-20652-9_11"},{"key":"22_CR48","doi-asserted-by":"crossref","unstructured":"Goel, A., Sakallah, K.A.: AVR: abstractly verifying reachability. In: Proceedings of TACAS, pp. 413\u2013422 (2020)","DOI":"10.1007\/978-3-030-45190-5_23"},{"key":"22_CR49","unstructured":"Goel, A., Krstic, S., Leslie, R., Tuttle, M.R.: SMT-based system verification with DVF. In: Proceedings of SMT Workshop, pp. 32\u201343 (2012)"},{"key":"22_CR50","doi-asserted-by":"crossref","unstructured":"Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Proceedings of FMCAD, pp. 1\u20139 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"22_CR51","doi-asserted-by":"crossref","unstructured":"Ho, Y., Mishchenko, A., Brayton, R.K.: Property directed reachability with word-level abstraction. In: Proceedings of FMCAD, pp. 132\u2013139 (2017)","DOI":"10.23919\/FMCAD.2017.8102251"},{"key":"22_CR52","unstructured":"Holzmann, G.J.: The SPIN Model Checker - primer and reference manual (2004)"},{"key":"22_CR53","doi-asserted-by":"crossref","unstructured":"Irfan, A., Cimatti, A., Griggio, A., Roveri, M., Sebastiani, R.: Verilog2SMV: a tool for word-level verification. In: Proceedings of DATE, pp. 1156\u20131159 (2016)","DOI":"10.3850\/9783981537079_0765"},{"key":"22_CR54","doi-asserted-by":"crossref","unstructured":"Jovanovic, D., Dutertre, B.: Property-directed k-induction. In: Proceedings of FMCAD, pp. 85\u201392 (2016)","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"22_CR55","doi-asserted-by":"crossref","unstructured":"K., H.G.V., Fedyukovich, G., Gurfinkel, A.: Word level property directed reachability. In: Proceedings of ICCAD, pp. 107:1\u2013107:9 (2020)","DOI":"10.1145\/3400302.3415708"},{"key":"22_CR56","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., et al.: Automatic abstraction in SMT-based unbounded software model checking. In: Proceedings of CAV, pp. 846\u2013862 (2013)","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"22_CR57","doi-asserted-by":"crossref","unstructured":"Kroening, D., Groce, A., Clarke, E.M.: Counterexample guided abstraction refinement via program execution. In: Proceedings of ICFEM, pp. 224\u2013238 (2004)","DOI":"10.1007\/978-3-540-30482-1_23"},{"key":"22_CR58","doi-asserted-by":"crossref","unstructured":"Mann, M., Irfan, A., et al.: Counterexample-guided prophecy for model checking modulo the theory of arrays. In: Proceedings of TACAS, pp. 113\u2013132 (2021)","DOI":"10.1007\/978-3-030-72016-2_7"},{"key":"22_CR59","doi-asserted-by":"crossref","unstructured":"Mann, M., Wilson, A., et al.: SMT-Switch: a Solver-agnostic C++ API for SMT Solving. In: Proceedings of SAT (2021)","DOI":"10.1007\/978-3-030-80223-3_26"},{"key":"22_CR60","doi-asserted-by":"crossref","unstructured":"Mattarei, C., Mann, M., Barrett, C., et al.: CoSA: Integrated verification for agile hardware design. In: Proceedings of FMCAD, pp. 1\u20135 (2018)","DOI":"10.23919\/FMCAD.2018.8603014"},{"key":"22_CR61","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Symbolic model checking - an approach to the state explosion problem. Ph.D. thesis, Carnegie Mellon University (1992)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"22_CR62","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolants and symbolic model checking. In: Proceedings of VMCAI, pp. 89\u201390 (2007)","DOI":"10.1007\/978-3-540-69738-1_6"},{"key":"22_CR63","doi-asserted-by":"crossref","unstructured":"McMillan, K.L., Padon, O.: Ivy: a multi-modal verification tool for distributed algorithms. In: Proceedings of CAV, pp. 190\u2013202 (2020)","DOI":"10.1007\/978-3-030-53291-8_12"},{"key":"22_CR64","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"22_CR65","doi-asserted-by":"crossref","unstructured":"de Moura, L., et al.: Sal 2. In: Proceedings of CAV, pp. 496\u2013500 (2004)","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"22_CR66","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC and Boolector 3.0. In: Proceedings of CAV, pp. 587\u2013595 (2018)","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"22_CR67","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"22_CR68","doi-asserted-by":"crossref","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Proceedings of FMCAD, pp. 108\u2013125 (2000)","DOI":"10.1007\/3-540-40922-X_8"},{"key":"22_CR69","unstructured":"Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 131\u2013153 (2009)"},{"key":"22_CR70","doi-asserted-by":"crossref","unstructured":"Tonetta, S.: Abstract model checking without computing the abstraction. In: Proceedings of FM, pp. 89\u2013105 (2009)","DOI":"10.1007\/978-3-642-05089-3_7"},{"key":"22_CR71","doi-asserted-by":"crossref","unstructured":"Welp, T., Kuehlmann, A.: QF BV model checking with property directed reachability. In: Proceedings of DATE, pp. 791\u2013796 (2013)","DOI":"10.7873\/DATE.2013.168"},{"key":"22_CR72","unstructured":"Wolf, C., Glaser, J., Kepler, J.: Yosys-a free Verilog synthesis suite. In: Proceedings of Austrochip Workshop (2013)"},{"key":"22_CR73","doi-asserted-by":"crossref","unstructured":"Zhang, H., Gupta, A., Malik, S.: Syntax-guided synthesis for lemma generation in hardware model checking. In: Proceedings of VMCAI (2021)","DOI":"10.1007\/978-3-030-67067-2_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-030-81688-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:25:03Z","timestamp":1626452703000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81688-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816872","9783030816889"],"references-count":73,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","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":"290","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":"63","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":"0","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":"22% - 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":"16 tool papers and 5 invited papers are also included.","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)"}}]}}