{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:41:10Z","timestamp":1768002070113,"version":"3.49.0"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720124","type":"print"},{"value":"9783030720131","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,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"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 present an approach to synthesize relational invariants to prove equivalences between object-oriented programs. The approach bridges the gap between recursive data types and arrays that serve to represent internal states. Our relational invariants are recursively-defined, and thus are valid for data structures of unbounded size. Based on introducing recursion into the proofs by observing and lifting the constraints from joint methods of the two objects, our approach is fully automatic and can be seen as an algorithm for solving Constrained Horn Clauses (CHC) of a specific sort. It has been implemented on top of the SMT-based CHC solver <jats:sc>AdtChc<\/jats:sc> and evaluated on a range of benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_2","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"24-42","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Bridging Arrays and ADTs in Recursive Proofs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1727-4043","authenticated-orcid":false,"given":"Grigory","family":"Fedyukovich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3289-5764","authenticated-orcid":false,"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. Modeling in Event-B: System and Software engineering. Cambridge University Press, 2010.","DOI":"10.1017\/CBO9781139195881"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"R.\u00a0Alur, R.\u00a0Bod\u00edk, G.\u00a0Juniwal, M.\u00a0M.\u00a0K. Martin, M.\u00a0Raghothaman, S.\u00a0A. Seshia, R.\u00a0Singh, A.\u00a0Solar-Lezama, E.\u00a0Torlak, and A.\u00a0Udupa. Syntax-Guided Synthesis. In FMCAD, pages 1\u201317. IEEE, 2013.","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"S.\u00a0Amani, A.\u00a0Hixon, Z.\u00a0Chen, C.\u00a0Rizkallah, P.\u00a0Chubb, L.\u00a0O\u2019Connor, J.\u00a0Beeren, Y.\u00a0Nagashima, J.\u00a0Lim, T.\u00a0Sewell, J.\u00a0Tuong, G.\u00a0Keller, T.\u00a0Murray, G.\u00a0Klein, and G.\u00a0Heiserer. Cogent: Verifying high-assurance file system implementations. In ASPLOS, pages 175\u2013188. ACM, 2016.","DOI":"10.1145\/2954680.2872404"},{"key":"2_CR4","unstructured":"R.-J. Back and J.\u00a0Wright. Refinement calculus: a systematic introduction. Springer Science & Business Media, 2012."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"G.\u00a0Barthe, J.\u00a0M. Crespo, and C.\u00a0Kunz. Relational verification using product programs. In FM, volume 6664 of LNCS, pages 200\u2013214. Springer, 2011.","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"C.\u00a0Baumann, B.\u00a0Beckert, H.\u00a0Blasum, and T.\u00a0Bormer. Lessons learned from microkernel verification\u2013specification is the new bottleneck. In SSV, volume 102 of EPTCS, pages 18\u201332. Elsevier, 2012.","DOI":"10.4204\/EPTCS.102.4"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"D.\u00a0Beyer and M.\u00a0E. Keremoglu. CPAchecker: A Tool for Configurable Software Verification. In CAV, volume 6806 of LNCS, pages 184\u2013190. Springer, 2011.","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"E.\u00a0B\u00f6rger. The ASM refinement method. Formal Aspects of Computing, 15(2-3):237\u2013257, 2003.","DOI":"10.1007\/s00165-003-0012-7"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"A.\u00a0Champion, N.\u00a0Kobayashi, and R.\u00a0Sato. HoIce: An ICE-Based Non-linear Horn Clause Solver. In APLAS, volume 11275 of LNCS, pages 146\u2013156. Springer, 2018.","DOI":"10.1007\/978-3-030-02768-1_8"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"H.\u00a0Chen, D.\u00a0Ziegler, A.\u00a0Chlipala, N.\u00a0Zeldovich, and M.\u00a0F. Kaashoek. Using Crash Hoare Logic for certifying the FSCQ file system. In SOSP. ACM, 2015.","DOI":"10.1145\/2815400.2815402"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"N.\u00a0Chong, B.\u00a0Cook, K.\u00a0Kallas, K.\u00a0Khazem, F.\u00a0R. Monteiro, D.\u00a0Schwartz-Narbonne, S.\u00a0Tasiran, M.\u00a0Tautschnig, and M.\u00a0R. Tuttle. Code-level model checking in the software development workflow. In G.\u00a0Rothermel and D.\u00a0Bae, editors, ICSE-SEIP, pages 11\u201320. ACM, 2020.","DOI":"10.1145\/3377813.3381347"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"A.\u00a0Chudnov, N.\u00a0Collins, B.\u00a0Cook, J.\u00a0Dodds, B.\u00a0Huffman, C.\u00a0MacC\u00e1rthaigh, S.\u00a0Magill, E.\u00a0Mertens, E.\u00a0Mullen, S.\u00a0Tasiran, et\u00a0al. Continuous formal verification of Amazon s2n. In CAV, pages 430\u2013446. Springer, 2018.","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"C.\u00a0L. Conway and C.\u00a0W. Barrett. Verifying low-level implementations of high-level datatypes. In CAV, volume 6174 of LNCS, pages 306\u2013320. Springer, 2010.","DOI":"10.1007\/978-3-642-14295-6_28"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"E.\u00a0De Angelis, F.\u00a0Fioravanti, A.\u00a0Pettorossi, and M.\u00a0Proietti. Solving Horn Clauses on Inductive Data Types Without Induction. TPLP, 18(3-4):452\u2013469, 2018.","DOI":"10.1017\/S1471068418000157"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"W.-P. de\u00a0Roever and K.\u00a0Engelhardt. Data refinement: Model-oriented proof methods and their comparison. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9780511663079"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"E.\u00a0W. Dijkstra. A constructive approach to the problem of program correctness. BIT Numerical Mathematics, 8(3):174\u2013186, 1968.","DOI":"10.1007\/BF01933419"},{"key":"2_CR17","unstructured":"G.\u00a0Ernst, J.\u00a0Pf\u00e4hler, G.\u00a0Schellhorn, D.\u00a0Haneberg, and W.\u00a0Reif. KIV: Overview and VerifyThis competition. Software Tools for Technology Transfer (STTT), 17(6):677\u2013694, 2015."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"G.\u00a0Fedyukovich, A.\u00a0Gurfinkel, and N.\u00a0Sharygina. Automated discovery of simulation between programs. In LPAR, volume 9450 of LNCS, pages 606\u2013621. Springer, 2015.","DOI":"10.1007\/978-3-662-48899-7_42"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"G.\u00a0Fedyukovich, S.\u00a0Kaufman, and R.\u00a0Bod\u00edk. Sampling Invariants from Frequency Distributions. In FMCAD, pages 100\u2013107. IEEE, 2017.","DOI":"10.23919\/FMCAD.2017.8102247"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"G.\u00a0Fedyukovich, S.\u00a0Prabhu, K.\u00a0Madhukar, and A.\u00a0Gupta. Solving Constrained Horn Clauses Using Syntax and Data. In FMCAD, pages 170\u2013178. IEEE, 2018.","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"G.\u00a0Fedyukovich, S.\u00a0Prabhu, K.\u00a0Madhukar, and A.\u00a0Gupta. Quantified Invariants via Syntax-Guided Synthesis. In CAV, Part I, volume 11561 of LNCS, pages 259\u2013277. Springer, 2019.","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"D.\u00a0Felsing, S.\u00a0Grebing, V.\u00a0Klebanov, P.\u00a0R\u00fcmmer, and M.\u00a0Ulbrich. Automating regression verification. In ASE, pages 349\u2013360. ACM, 2014.","DOI":"10.1145\/2642937.2642987"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"B.\u00a0Godlin and O.\u00a0Strichman. Inference rules for proving the equivalence of recursive procedures. Acta Informatica, 45(6):403\u2013439, 2008.","DOI":"10.1007\/s00236-008-0075-2"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"A.\u00a0Gurfinkel, T.\u00a0Kahsai, A.\u00a0Komuravelli, and J.\u00a0A. Navas. The SeaHorn Verification Framework. In CAV, volume 9206 of LNCS, pages 343\u2013361. Springer, 2015.","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"J.\u00a0He, C.\u00a0A.\u00a0R. Hoare, and J.\u00a0W. Sanders. Data refinement refined. In ESOP, pages 187\u2013196. Springer, 1986.","DOI":"10.1007\/3-540-16442-1_14"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"C.\u00a0A.\u00a0R. Hoare. Unified theories of programming. In Mathematical methods in program development, pages 313\u2013367. Springer, 1997.","DOI":"10.1007\/978-3-642-60858-2_21"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"H.\u00a0Hojjat and P.\u00a0R\u00fcmmer. The ELDARICA Horn Solver. In FMCAD, pages 158\u2013164. IEEE, 2018.","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"J.\u00a0P. Inala, N.\u00a0Polikarpova, X.\u00a0Qiu, B.\u00a0S. Lerner, and A.\u00a0Solar-Lezama. Synthesis of recursive ADT transformations from reusable templates. In TACAS, Part I, volume 10205 of LNCS, pages 247\u2013263, 2017.","DOI":"10.1007\/978-3-662-54577-5_14"},{"key":"2_CR29","unstructured":"C.\u00a0B. Jones. Systematic software development using VDM, volume\u00a02. Prentice Hall Englewood Cliffs, 1990."},{"key":"2_CR30","unstructured":"G.\u00a0Klein, J.\u00a0Andronick, K.\u00a0Elphinstone, G.\u00a0Heiser, D.\u00a0Cock, P.\u00a0Derrin, D.\u00a0Elkaduwe, K.\u00a0Engelhardt, R.\u00a0Kolanski, M.\u00a0Norrish, T.\u00a0Sewell, H.\u00a0Tuch, and S.\u00a0Winwood.\u00a0seL4: Formal verification of an operating-system kernel. Communications of the ACM, 53(6):107\u2013115, 2010."},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"E.\u00a0Kneuss, I.\u00a0Kuraj, V.\u00a0Kuncak, and P.\u00a0Suter. Synthesis modulo recursive functions. In OOPSLA, pages 407\u2013426, 2013.","DOI":"10.1145\/2544173.2509555"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"A.\u00a0Komuravelli, A.\u00a0Gurfinkel, and S.\u00a0Chaki. SMT-Based Model Checking for Recursive Programs. In CAV, volume 8559 of LNCS, pages 17\u201334, 2014.","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"2_CR33","unstructured":"L.\u00a0Lamport. Specifying systems: the $$TLA^+$$ language and tools for hardware and software engineers. Addison-Wesley, 2002."},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"K.\u00a0R.\u00a0M. Leino and A.\u00a0Milicevic. Program extrapolation with Jennisys. In OOPSLA, pages 411\u2013430, 2012.","DOI":"10.1145\/2398857.2384646"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"X.\u00a0Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107\u2013115, 2009.","DOI":"10.1145\/1538788.1538814"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"B.\u00a0H. Liskov and J.\u00a0M. Wing. A behavioral notion of subtyping. Transactions on Programming Languages and Systems, 16(6):1811\u20131841, 1994.","DOI":"10.1145\/197320.197383"},{"key":"2_CR37","unstructured":"R.\u00a0Milner. An algebraic definition of simulation between programs. In IJCAI, pages 481\u2013489, 1971."},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"A.\u00a0Miltner, S.\u00a0Padhi, T.\u00a0Millstein, and D.\u00a0Walker. Data-driven inference of representation invariants. In PLDI, pages 1\u201315, 2020.","DOI":"10.1145\/3395638"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"D.\u00a0Mordvinov and G.\u00a0Fedyukovich. Property Directed Inference of Relational Invariants. In FMCAD, pages 152\u2013160. IEEE, 2019.","DOI":"10.23919\/FMCAD.2019.8894274"},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"L.\u00a0D. Moura and N.\u00a0Bj\u00f8rner. Z3: An efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337\u2013340. Springer, 2008.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"K.\u00a0S. Namjoshi and L.\u00a0D. Zuck. Witnessing program transformations. In SAS, volume 7935 of LNCS, pages 304\u2013323. Springer, 2013.","DOI":"10.1007\/978-3-642-38856-9_17"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"L.\u00a0Nelson, H.\u00a0Sigurbjarnarson, K.\u00a0Zhang, D.\u00a0Johnson, J.\u00a0Bornholt, E.\u00a0Torlak, and X.\u00a0Wang. Hyperkernel: Push-button verification of an OS kernel. In OSDI, pages 252\u2013269, 2017.","DOI":"10.1145\/3132747.3132748"},{"key":"2_CR43","doi-asserted-by":"crossref","unstructured":"P.\u00a0W. O\u2019Hearn. Continuous reasoning: scaling the impact of formal methods. In LICS, pages 13\u201325. ACM, 2018.","DOI":"10.1145\/3209108.3209109"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"L.\u00a0Pick, G.\u00a0Fedyukovich, and A.\u00a0Gupta. Exploiting Synchrony and Symmetry in Relational Verification. In CAV, Part I, volume 10981 of LNCS, pages 164\u2013182. Springer, 2018.","DOI":"10.1007\/978-3-319-96145-3_9"},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"M.-L. Potet and Y.\u00a0Rouzaud. Composition and refinement in the B-method. In Proc. of the B Conference, volume 1393 of LNCS, pages 46\u201365. Springer, 1998.","DOI":"10.1007\/BFb0053355"},{"key":"2_CR46","doi-asserted-by":"crossref","unstructured":"A.\u00a0Reynolds, H.\u00a0Barbosa, A.\u00a0N\u00f6tzli, C.\u00a0W. Barrett, and C.\u00a0Tinelli. cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. In CAV, Part II, volume 11562 of LNCS, pages 74\u201383. Springer, 2019.","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"2_CR47","doi-asserted-by":"crossref","unstructured":"A.\u00a0Reynolds and V.\u00a0Kuncak. Induction for SMT solvers. In VMCAI, volume 8931 of LNCS, pages 80\u201398. Springer, 2015.","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"2_CR48","doi-asserted-by":"crossref","unstructured":"G.\u00a0Schellhorn, G.\u00a0Ernst, J.\u00a0Pf\u00e4hler, D.\u00a0Haneberg, and W.\u00a0Reif. Development of a verified Flash file system. In ABZ, volume 8477 of LNCS, pages 9\u201324. Springer, 2014. Invited Paper.","DOI":"10.1007\/978-3-662-43652-3_2"},{"key":"2_CR49","doi-asserted-by":"crossref","unstructured":"R.\u00a0Sharma, E.\u00a0Schkufza, B.\u00a0R. Churchill, and A.\u00a0Aiken. Data-driven Equivalence Checking. In OOPSLA, pages 391\u2013406. ACM, 2013.","DOI":"10.1145\/2544173.2509509"},{"key":"2_CR50","unstructured":"H.\u00a0Sigurbjarnarson, J.\u00a0Bornholt, E.\u00a0Torlak, and X.\u00a0Wang. Push-button verification of file systems via crash refinement. In OSDI, pages 1\u201316, 2016."},{"key":"2_CR51","doi-asserted-by":"crossref","unstructured":"O.\u00a0Strichman and M.\u00a0Veitsman. Regression verification for unbalanced recursive functions. In FM, pages 645\u2013658. Springer, 2016.","DOI":"10.1007\/978-3-319-48989-6_39"},{"key":"2_CR52","doi-asserted-by":"crossref","unstructured":"P.\u00a0Suter, M.\u00a0Dotta, and V.\u00a0Kuncak. Decision procedures for algebraic data types with abstractions. SIGPLAN notices, 45(1):199\u2013210, 2010.","DOI":"10.1145\/1707801.1706325"},{"key":"2_CR53","doi-asserted-by":"crossref","unstructured":"H.\u00a0Unno, S.\u00a0Torii, and H.\u00a0Sakamoto. Automating Induction for Solving Horn Clauses. In CAV, volume 10427 of LNCS, pages 571\u2013591. Springer, 2017.","DOI":"10.1007\/978-3-319-63390-9_30"},{"key":"2_CR54","doi-asserted-by":"crossref","unstructured":"N.\u00a0Wirth. Program development by stepwise refinement. Communications of the ACM, 14(4):221\u2013227, 1971.","DOI":"10.1145\/362575.362577"},{"key":"2_CR55","doi-asserted-by":"crossref","unstructured":"W.\u00a0Yang, G.\u00a0Fedyukovich, and A.\u00a0Gupta. Lemma Synthesis for Automating Induction over Algebraic Data Types. In CP, volume 11802 of LNCS, pages 600\u2013617. Springer, 2019.","DOI":"10.1007\/978-3-030-30048-7_35"},{"key":"2_CR56","doi-asserted-by":"crossref","unstructured":"A.\u00a0Zaostrovnykh, S.\u00a0Pirelli, R.\u00a0Iyer, M.\u00a0Rizzo, L.\u00a0Pedrosa, K.\u00a0Argyraki, and G.\u00a0Candea. Verifying software network functions with no verification expertise. In OSDI, pages 275\u2013290, 2019.","DOI":"10.1145\/3341301.3359647"}],"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-72013-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:09:40Z","timestamp":1616436580000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_2","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":"23 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)"}}]}}