{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:52:10Z","timestamp":1760043130329,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030816841"},{"type":"electronic","value":"9783030816858"}],"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>Formal methods are becoming an indispensable part of the design process in software and hardware industry. It takes robust tools and proofs to make formal validation of large scale projects reliable. In this paper, we will describe the current status of formal verification at Centaur Technology. We will explain our challenges and our methodology\u2014how various proofs and verification artifacts are interconnected and how we keep them consistent over the duration of a project. We also describe our main engine\u2014a powerful symbolic simulator with rewriting capabilities that is integrated in a theorem prover and proven correct.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_2","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"26-45","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Balancing Automation and Control for Formal Verification of Microprocessors"],"prefix":"10.1007","author":[{"given":"Shilpi","family":"Goel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anna","family":"Slobodova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rob","family":"Sumners","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sol","family":"Swords","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"2_CR1","unstructured":"ACL2 Documentation: AIGNET-ABC-INTERFACE Interface to ABC. Accessed April 2021. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v8-3\/combined-manual\/?topic=AIGNET_AIGNET-ABC-INTERFACE"},{"key":"2_CR2","unstructured":"ACL2 Documentation: CLAUSE-PROCESSOR. Accessed April 2021. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v8-3\/combined-manual\/?topic=ACL2_CLAUSE-PROCESSOR"},{"key":"2_CR3","unstructured":"ACL2 Documentation: FAST-ALISTS. Accessed April 2021. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v8-3\/combined-manual\/?topic=ACL2_FAST-ALISTS"},{"key":"2_CR4","unstructured":"ACL2 Documentation: FGL Bit-blasting Prover Framework. Accessed April 2021. https:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v8-3\/combined-manual\/?topic=FGL_FGL"},{"key":"2_CR5","unstructured":"ACL2 Documentation: SMTLINK Interface to Z3. Accessed April 2021. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v8-3\/combined-manual\/?topic=SMT_SMTLINK"},{"key":"2_CR6","unstructured":"ACL2 Documentation: SV Hardware Verification Library. Accessed April 2021. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v8-3\/combined-manual\/?topic=ACL2_SV"},{"key":"2_CR7","unstructured":"ACL2 Documentation: VL Verilog Toolkit. Accessed April 2021. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v8-3\/combined-manual\/?topic=ACL2_VL"},{"key":"2_CR8","unstructured":"ACL2 Home Page. Accessed April 2021. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2"},{"key":"2_CR9","unstructured":"FGL Library in the ACL2 Community Books. Accessed April 2021. https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/centaur\/fgl"},{"key":"2_CR10","unstructured":"VL Verilog Toolkit. Accessed: April 2021. https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/centaur\/vl"},{"key":"2_CR11","unstructured":"Anderson, S.E.: Bit twiddling hacks. Accessed: April 2021. https:\/\/graphics.stanford.edu\/~seander\/bithacks.html#CountBitsSetParallel"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"101","DOI":"10.6092\/issn.1972-5787\/4593","volume":"9","author":"J Blanchette","year":"2016","unstructured":"Blanchette, J., Kaliszyk, C., Paulson, L., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4593","journal-title":"J. Formaliz. Reason."},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Boyer, R.S., Hunt, Jr., W.A.: Symbolic simulation in ACL2. In: Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 2009, pp. 20\u201324. ACM, New York (2009). https:\/\/doi.org\/10.1145\/1637837.1637840","DOI":"10.1145\/1637837.1637840"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"issue":"3","key":"2_CR15","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992). https:\/\/doi.org\/10.1145\/136035.136043","journal-title":"ACM Comput. Surv."},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-96145-3_3","volume-title":"Computer Aided Verification","author":"B Cook","year":"2018","unstructured":"Cook, B.: Formal reasoning about the security of Amazon web services. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018, Part I. LNCS, vol. 10981, pp. 38\u201347. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_3"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Davis, J., Kaufmann, M.: Industrial-strength documentation for ACL2. In: Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2014, Vienna, Austria, 12\u201313 July 2014, pp. 9\u201325 (2014). https:\/\/doi.org\/10.4204\/EPTCS.152.2","DOI":"10.4204\/EPTCS.152.2"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-08970-6_1","volume-title":"Interactive Theorem Proving","author":"J Davis","year":"2014","unstructured":"Davis, J., Slobodova, A., Swords, S.: Microcode verification \u2013 another piece of the microprocessor verification puzzle. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 1\u201316. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_1"},{"key":"2_CR19","unstructured":"Dill, D.L.: Formal Verification of Libra Blockchain Smart Contracts. Recording of the keynote (2020). https:\/\/www.youtube.com\/watch?v=cYxxJU-Wt2U"},{"key":"2_CR20","unstructured":"Goel, S.: Formal Verification of Application and System Programs Based on a Validated x86 ISA Model. Ph.D. thesis, Department of Computer Science, The University of Texas at Austin (2016). http:\/\/hdl.handle.net\/2152\/46437"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Goel, S., Slobodova, A., Sumners, R., Swords, S.: Verifying x86 instruction implementations. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 47\u201360. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3372885.3373811","DOI":"10.1145\/3372885.3373811"},{"key":"2_CR22","unstructured":"Greve, D., Wilding, M.: Evaluatable, high-assurance microprocessors. In: NSA High-Confidence Systems and Software Conference (HCSS), Linthicum, MD, March 2002. http:\/\/hokiepokie.org\/docs\/hcss02\/proceedings.pdf"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/11541868_11","volume-title":"Theorem Proving in Higher Order Logics","author":"WA Hunt","year":"2005","unstructured":"Hunt, W.A., Kaufmann, M., Krug, R.B., Moore, J.S., Smith, E.W.: Meta reasoning in ACL2. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 163\u2013178. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_11"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Hunt, Jr., W.A., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with ACL2. In: Verified Trustworthy Software Systems, vol. 375. The Royal Society (2017). https:\/\/doi.org\/10.1098\/rsta.2015.0399 (Article Number 20150399)","DOI":"10.1098\/rsta.2015.0399"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-02658-4_28","volume-title":"Computer Aided Verification","author":"WA Hunt","year":"2009","unstructured":"Hunt, W.A., Swords, S.: Centaur technology media unit verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 353\u2013367. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_28"},{"key":"2_CR26","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-1-4419-1539-9_3","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"WAA Hunt, Jr.","year":"2010","unstructured":"Hunt, Jr., W.A.A., Swords, S., Davis, J., Slobodova, A.: Use of formal verification at centaur technology. In: Hardin, D. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 65\u201388. Springer, Boston (2010). https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_3"},{"key":"2_CR27","unstructured":"Intel Corporation: Intel$$^{\\textregistered }$$ 64 and IA-32 Architectures Software Developer\u2019s Manual Combined Volumes: 1, 2A, 2B, 2C, 2D, 3A, 3B, 3C, 3D, and 4, November, 2020, Order Number: 325462\u2013070US. https:\/\/software.intel.com\/en-us\/articles\/intel-sdm"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-02658-4_32","volume-title":"Computer Aided Verification","author":"R Kaivola","year":"2009","unstructured":"Kaivola, R., et al.: Replacing testing with formal verification in Intel\u00ae Core$$^{\\rm TM}$$ i7 processor execution engine validation. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 414\u2013429. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_32"},{"key":"2_CR29","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/s10817-018-09505-9","volume":"64","author":"M Kaufmann","year":"2020","unstructured":"Kaufmann, M., Moore, J.S.: Limited second-order functionality in the first-order setting. J. Autom. Reason. 64, 391\u2013422 (2020). https:\/\/doi.org\/10.1007\/s10817-018-09505-9","journal-title":"J. Autom. Reason."},{"key":"2_CR30","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Formal reasoning and the hacker way (keynote). In: Krishnan, P., Reichenbach, C. (eds.) Proceedings of the 9th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, SOAP@PLDI 2020, London, UK, 15 June 2020, p. 1. ACM (2020). https:\/\/doi.org\/10.1145\/3394451.3401953","DOI":"10.1145\/3394451.3401953"},{"key":"2_CR31","doi-asserted-by":"publisher","unstructured":"Peng, Y., Greenstreet, M.R.: Smtlink 2.0. In: Electronic Proceedings in Theoretical Computer Science, vol. 280, pp. 143\u2013160, October 2018. https:\/\/doi.org\/10.4204\/eptcs.280.11","DOI":"10.4204\/eptcs.280.11"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Rager, D.L., Ebergen, J., Nadezhin, D., Lee, A., Chau, C., Selfridge, B.: Formal Verification of Division and Square Root Implementations, an Oracle Report, pp. 149\u2013160. ACM, IEEE, October 2016","DOI":"10.1109\/FMCAD.2016.7886673"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/11814771_38","volume-title":"Automated Reasoning","author":"E Reeber","year":"2006","unstructured":"Reeber, E., Hunt, W.A.: A SAT-based decision procedure for the subclass of unrollable list formulas in ACL2 (SULFA). In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 453\u2013467. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_38"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-41540-6_3","volume-title":"Computer Aided Verification","author":"A Reid","year":"2016","unstructured":"Reid, A., et al.: End-to-end verification of processors with ISA-formal. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part II. LNCS, vol. 9780, pp. 42\u201358. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_3"},{"key":"2_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95513-1","volume-title":"Formal Verification of Floating-Point Hardware Design: A Mathematical Approach","author":"DM Russinoff","year":"2019","unstructured":"Russinoff, D.M.: Formal Verification of Floating-Point Hardware Design: A Mathematical Approach. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-95513-1"},{"key":"2_CR36","unstructured":"Sawada, J., Sandon, P., Paruthi, V., Baumgartner, J., Case, M., Mony, H.: Hybrid verification of a hardware modular reduction engine. In: Bjesse, P., Slobodova, A. (eds.) Proceedings of Formal Methods in Computer-Aided Design (FMCAD). ACM\/IEEE CEDA (2011). https:\/\/www.cs.utexas.edu\/users\/hunt\/FMCAD\/FMCAD11\/"},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"Slobodova, A., Davis, J., Swords, S., Hunt, Jr., W.A.: A flexible formal verification framework for industrial scale validation. In: Proceedings of the $$9$$th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 89\u201397. IEEE\/ACM, Cambridge (2011). https:\/\/doi.org\/10.1109\/memcod.2011.5970515","DOI":"10.1109\/memcod.2011.5970515"},{"key":"2_CR38","doi-asserted-by":"publisher","unstructured":"Swords, S.: Term-level reasoning in support of bit-blasting. In: Slobodova, A., Hunt, Jr., W.A. (eds.) Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 22\u201323 May 2017. Electronic Proceedings in Theoretical Computer Science, vol. 249, pp. 95\u2013111. Open Publishing Association (2017). https:\/\/doi.org\/10.4204\/EPTCS.249.7","DOI":"10.4204\/EPTCS.249.7"},{"key":"2_CR39","doi-asserted-by":"publisher","unstructured":"Swords, S.: New rewriter features in FGL. In: Passmore, G., Gamboa, R. (eds.) Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, 28\u201329 May 2020. Electronic Proceedings in Theoretical Computer Science, vol. 327, pp. 32\u201346. Open Publishing Association (2020). https:\/\/doi.org\/10.4204\/EPTCS.327.3","DOI":"10.4204\/EPTCS.327.3"},{"key":"2_CR40","unstructured":"Swords, S.: FGL example. Accessed April 2021. https:\/\/github.com\/solswords\/fgl-example"},{"key":"2_CR41","doi-asserted-by":"publisher","unstructured":"Swords, S., Davis, J.: Bit-blasting ACL2 theorems. In: Hardin, D., Schmaltz, J. (eds.) Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 3\u20134 November 2011. Electronic Proceedings in Theoretical Computer Science, vol. 70, pp. 84\u2013102. Open Publishing Association (2011). https:\/\/doi.org\/10.4204\/EPTCS.70.7","DOI":"10.4204\/EPTCS.70.7"},{"key":"2_CR42","unstructured":"Swords, S.O.: A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. Ph.D. thesis, University of Texas at Austin, December 2010. http:\/\/hdl.handle.net\/2152\/ETD-UT-2010-12-2210"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-030-53288-8_23","volume-title":"Computer Aided Verification","author":"M Temel","year":"2020","unstructured":"Temel, M., Slobodova, A., Hunt, W.A.: Automated and scalable verification of integer multipliers. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 485\u2013507. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_23"},{"key":"2_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-030-53288-8_7","volume-title":"Computer Aided Verification","author":"JE Zhong","year":"2020","unstructured":"Zhong, J.E., et al.: The move prover. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020, Part I. LNCS, vol. 12224, pp. 137\u2013150. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_7"}],"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-81685-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:47Z","timestamp":1626480167000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_2","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":"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)"}}]}}