{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:16:56Z","timestamp":1760203016239,"version":"3.40.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030995263"},{"type":"electronic","value":"9783030995270"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose several heuristics for mitigating one of the main causes of combinatorial explosion in rank-based complementation of B\u00fcchi automata (BAs): unnecessarily high bounds on the ranks of states. First, we identify<jats:italic>elevator automata<\/jats:italic>, which is a\u00a0large class of BAs (generalizing semi-deterministic BAs), occurring often in practice, where ranks of states are bounded according to the structure of strongly connected components. The bounds for elevator automata also carry over to general BAs that contain elevator automata as a\u00a0sub-structure. Second, we introduce two techniques for refining bounds on the ranks of BA states using data-flow analysis of the automaton. We implement out techniques as an extension of the tool<jats:sc>Ranker<\/jats:sc>for BA complementation and show that they indeed greatly prune the generated state space, obtaining significantly better results and outperforming other state-of-the-art tools on a\u00a0large set of benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_7","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T10:37:21Z","timestamp":1648550241000},"page":"118-136","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Sky Is Not the Limit"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4375-7954","authenticated-orcid":false,"given":"Vojt\u011bch","family":"Havlena","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1184-4669","authenticated-orcid":false,"given":"Barbora","family":"\u0160mahl\u00edkov\u00e1","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Allred, J.D., Ultes-Nitsche, U.: A simple and optimal complementation algorithm for B\u00fcchi automata. In: Proceedings of the Thirty third Annual IEEE Symposium on Logic in Computer Science (LICS 2018). pp. 46\u201355. IEEE Computer Society Press (July 2018)","DOI":"10.1145\/3209108.3209138"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., K\u0159et\u00ednsk\u00fd, J., M\u00fcller, D., Parker, D., Strej\u010dek, J.: The Hanoi omega-automata format. In: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol.\u00a09206, pp. 479\u2013486. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_31","DOI":"10.1007\/978-3-319-21690-4_31"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Blahoudek, F., Heizmann, M., Schewe, S., Strej\u010dek, J., Tsai, M.H.: Complementing semi-deterministic b\u00fcchi automata. In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 770\u2013787. Springer Berlin Heidelberg, Berlin, Heidelberg (2016)","DOI":"10.1007\/978-3-662-49674-9_49"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Blahoudek, F., Duret-Lutz, A., Strej\u010dek, J.: Seminator\u00a02 can complement generalized B\u00fcchi automata via improved semi-determinization. In: Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV\u201920). Lecture Notes in Computer Science, vol. 12225, pp. 15\u201327. Springer (Jul 2020)","DOI":"10.1007\/978-3-030-53291-8_2"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Blahoudek, F., Heizmann, M., Schewe, S., Strej\u010dek, J., Tsai, M.: Complementing semi-deterministic B\u00fcchi automata. In: Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09636, pp. 770\u2013787. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_49","DOI":"10.1007\/978-3-662-49674-9_49"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings. Lecture Notes in Computer Science, vol.\u00a02083, pp. 611\u2013625. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_50","DOI":"10.1007\/3-540-45744-5_50"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Breuers, S., L\u00f6ding, C., Olschewski, J.: Improved Ramsey-based B\u00fcchi complementation. In: Proc. of FOSSACS\u201912. pp. 150\u2013164. Springer (2012)","DOI":"10.1007\/978-3-642-28729-9_10"},{"key":"7_CR8","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. of International Congress on Logic, Method, and Philosophy of Science 1960. Stanford Univ. Press, Stanford (1962)"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Chen, Y., Havlena, V., Leng\u00e1l, O.: Simulations in rank-based B\u00fcchi automata complementation. In: Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11893, pp. 447\u2013467. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-34175-6_23","DOI":"10.1007\/978-3-030-34175-6_23"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Chen, Y., Heizmann, M., Leng\u00e1l, O., Li, Y., Tsai, M., Turrini, A., Zhang, L.: Advanced automata-based algorithms for program termination checking. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018. pp. 135\u2013150. ACM (2018). https:\/\/doi.org\/10.1145\/3192366.3192405","DOI":"10.1145\/3192366.3192405"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988. pp. 338\u2013345. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21950","DOI":"10.1109\/SFCS.1988.21950"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0 \u2014 a framework for LTL and $$\\omega $$-automata manipulation. In: Automated Technology for Verification and Analysis. pp. 122\u2013129. Springer International Publishing, Cham (2016)","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Fogarty, S., Vardi, M.Y.: B\u00fcchi complementation and size-change termination. In: Proc. of TACAS\u201909. pp. 16\u201330. Springer (2009)","DOI":"10.1007\/978-3-642-00768-2_2"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Friedgut, E., Kupferman, O., Vardi, M.: B\u00fcchi complementation made tighter. International Journal of Foundations of Computer Science 17, 851\u2013868 (2006)","DOI":"10.1142\/S0129054106004145"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic B\u00fcchi automata. In: Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L\u2019Aquila, Italy, October 21-24, 2003, Proceedings. LNCS, vol.\u00a02860, pp. 96\u2013110. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-39724-3_10","DOI":"10.1007\/978-3-540-39724-3_10"},{"key":"7_CR16","unstructured":"Havlena, V., Leng\u00e1l, O., Smahl\u00edkov\u00e1, B.: Sky is not the limit: Tighter rank bounds for elevator automata in B\u00fcchi automata complementation (technical report). CoRR abs\/2110.10187 (2021), https:\/\/arxiv.org\/abs\/2110.10187"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Havlena, V., Leng\u00e1l, O., \u0160mahl\u00edkov\u00e1, B.: Deciding S1S: Down the rabbit hole and through the looking glass. In: Proceedings of NETYS\u201921. pp. 215\u2013222. No. 12754 in LNCS, Springer Verlag (2021). https:\/\/doi.org\/10.1007\/978-3-030-91014-3_15","DOI":"10.1007\/978-3-030-91014-3_15"},{"key":"7_CR18","unstructured":"Havlena, V., Leng\u00e1l, O., \u0160mahl\u00edkov\u00e1, B.: Ranker (2021), https:\/\/github.com\/vhavlena\/ranker"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Havlena, V., Leng\u00e1l, O.: Reducing (To) the Ranks: Efficient Rank-Based B\u00fcchi Automata Complementation. In: Proc. of CONCUR\u201921. LIPIcs, vol.\u00a0203, pp. 2:1\u20132:19. Schloss Dagstuhl, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.2, iSSN: 1868-8969","DOI":"10.4230\/LIPIcs.CONCUR.2021.2"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Proc. of CAV\u201914. pp. 797\u2013813. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_53"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"K\u00e4hler, D., Wilke, T.: Complementation, disambiguation, and determinization of B\u00fcchi automata unified. In: Proc. of ICALP\u201908. pp. 724\u2013735. Springer (2008)","DOI":"10.1007\/978-3-540-70575-8_59"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Karmarkar, H., Chakraborty, S.: On minimal odd rankings for B\u00fcchi complementation. In: Proc. of ATVA\u201909. LNCS, vol.\u00a05799, pp. 228\u2013243. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-04761-9_18","DOI":"10.1007\/978-3-642-04761-9_18"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Klein, J., Baier, C.: On-the-fly stuttering in the construction of deterministic omega -automata. In: Proc. of CIAA\u201907. LNCS, vol.\u00a04783, pp. 51\u201361. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-76336-9_7","DOI":"10.1007\/978-3-540-76336-9_7"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(3), 408\u2013429 (2001). https:\/\/doi.org\/10.1145\/377978.377993","DOI":"10.1145\/377978.377993"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Kurshan, R.P.: Complementing deterministic B\u00fcchi automata in polynomial time. J. Comput. Syst. Sci. 35(1), 59\u201371 (1987). https:\/\/doi.org\/10.1016\/0022-0000(87)90036-5","DOI":"10.1016\/0022-0000(87)90036-5"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Li, Y., Sun, X., Turrini, A., Chen, Y., Xu, J.: ROLL 1.0: $$\\omega $$-regular language learning library. In: Proc. of TACAS\u201919. LNCS, vol. 11427, pp. 365\u2013371. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_23","DOI":"10.1007\/978-3-030-17462-0_23"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Li, Y., Turrini, A., Zhang, L., Schewe, S.: Learning to complement B\u00fcchi automata. In: Proc. of VMCAI\u201918. pp. 313\u2013335. Springer (2018)","DOI":"10.1007\/978-3-319-73721-8_15"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Li, Y., Vardi, M.Y., Zhang, L.: On the power of unambiguity in B\u00fcchi complementation. In: Proc. of GandALF\u201920. EPTCS, vol.\u00a0326, pp. 182\u2013198. Open Publishing Association (2020). https:\/\/doi.org\/10.4204\/EPTCS.326.12","DOI":"10.4204\/EPTCS.326.12"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C., Pirogov, A.: New optimizations and heuristics for determinization of b\u00fcchi automata. In: Automated Technology for Verification and Analysis. pp. 317\u2013333. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_18","DOI":"10.1007\/978-3-030-31784-3_18"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Mayr, R., Clemente, L.: Advanced automata minimization. In: Proc. of POPL\u201913. pp. 63\u201374 (2013)","DOI":"10.1145\/2480359.2429079"},{"key":"7_CR31","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris 15 (1988)"},{"key":"7_CR32","doi-asserted-by":"publisher","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis. Springer (1999). https:\/\/doi.org\/10.1007\/978-3-662-03811-6","DOI":"10.1007\/978-3-662-03811-6"},{"key":"7_CR33","unstructured":"Oei, R., Ma, D., Schulz, C., Hieronymi, P.: Pecan: An automated theorem prover for automatic sequences using b\u00fcchi automata. CoRR abs\/2102.01727 (2021), https:\/\/arxiv.org\/abs\/2102.01727"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: Proc. of LICS\u201906. pp. 255\u2013264. IEEE (2006)","DOI":"10.1109\/LICS.2006.28"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Redziejowski, R.R.: An improved construction of deterministic omega-automaton using derivatives. Fundam. Informaticae 119(3-4), 393\u2013406 (2012). https:\/\/doi.org\/10.3233\/FI-2012-744","DOI":"10.3233\/FI-2012-744"},{"key":"7_CR36","unstructured":"Safra, S.: On the complexity of $$\\omega $$-automata. In: Proc. of FOCS\u201988. pp. 319\u2013327. IEEE (1988)"},{"key":"7_CR37","doi-asserted-by":"publisher","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: Proc. of STACS\u201909. LIPIcs, vol.\u00a03, pp. 661\u2013672. Schloss Dagstuhl (2009). https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2009.1854","DOI":"10.4230\/LIPIcs.STACS.2009.1854"},{"key":"7_CR38","doi-asserted-by":"crossref","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The Complementation Problem for B\u00fcchi Automata with Applications to Temporal Logic. Theoretical Computer Science 49(2-3), 217\u2013237 (1987)","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Proc. of LPAR\u201905. pp. 396\u2013411. Springer (2005)","DOI":"10.1007\/11591191_28"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Tsai, M.H., Fogarty, S., Vardi, M.Y., Tsay, Y.K.: State of B\u00fcchi complementation. In: Implementation and Application of Automata. pp. 261\u2013271. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-18098-9_28"},{"key":"7_CR41","doi-asserted-by":"crossref","unstructured":"Tsai, M.H., Tsay, Y.K., Hwang, Y.S.: GOAL for games, omega-automata, and logics. In: Computer Aided Verification. pp. 883\u2013889. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39799-8_62"},{"key":"7_CR42","unstructured":"Vardi, M.Y., Wilke, T.: Automata: From logics to algorithms. Logic and Automata 2, 629\u2013736 (2008)"},{"key":"7_CR43","doi-asserted-by":"crossref","unstructured":"Yan, Q.: Lower bounds for complementation of $$\\omega $$-automata via the full automata technique. In: Automata, Languages and Programming. pp. 589\u2013600. Springer Berlin Heidelberg, Berlin, Heidelberg (2006)","DOI":"10.1007\/11787006_50"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99527-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,21]],"date-time":"2024-09-21T05:41:28Z","timestamp":1726897288000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_7"}},"subtitle":["Tighter Rank Bounds for Elevator Automata in B\u00fcchi Automata Complementation"],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","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":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/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":"159","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":"46","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":"4","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":"10","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 of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","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)"}}]}}