{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:05:37Z","timestamp":1776373537832,"version":"3.51.2"},"publisher-location":"Cham","reference-count":118,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030175016","type":"print"},{"value":"9783030175023","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17502-3_1","type":"book-chapter","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T05:19:26Z","timestamp":1554355166000},"page":"3-24","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":35,"title":["TOOLympics 2019: An Overview of Competitions in Formal Methods"],"prefix":"10.1007","author":[{"given":"Ezio","family":"Bartocci","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul E.","family":"Black","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hubert","family":"Garavel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabrice","family":"Kordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julian","family":"Nagele","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9619-1558","authenticated-orcid":false,"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tjark","family":"Weber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,4]]},"reference":[{"key":"1_CR1","unstructured":"Abate, A., Blom, H., Cauchi, N., Haesaert, S., Hartmanns, A., Lesser, K., Oishi, M., Sivaramakrishnan, V., Soudjani, S., Vasile, C.I., Vinod, A.P.: ARCH-COMP18 category report: Stochastic modelling. In: ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, vol. 54, pp. 71\u2013103 (2018). https:\/\/easychair.org\/publications\/open\/DzD8"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Amparore, E., Berthomieu, B., Ciardo, G., Dal Zilio, S., Gall\u00e0, F., Hillah, L.M., Hulin-Hubard, F., Jensen, P.G., Jezequel, L., Kordon, F., Le Botlan, D., Liebke, T., Meijer, J., Miner, A., Paviot-Adet, E., Srba,\u00a0J., Thierry-Mieg, Y., van Dijk, T., Wolf, K.: Presentation of the 9th edition of the model checking contest. In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 50\u201368. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_4","DOI":"10.1007\/978-3-030-17502-3_4"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Aoto, T., Hamana, M., Hirokawa, N., Middeldorp, A., Nagele, J., Nishida, N., Shintani, K., Zankl, H.: Confluence Competition 2018. In: Proc. 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 108, pp. 32:1\u201332:5. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2018.32","DOI":"10.4230\/LIPIcs.FSCD.2018.32"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Aoto, T., Hirokawa, N., Nagele, J., Nishida, N., Zankl, H.: Confluence Competition 2015. In: Proc. 25th International Conference on Automated Deduction (CADE-25), LNCS, vol.\u00a09195, pp. 101\u2013104. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_5","DOI":"10.1007\/978-3-319-21401-6_5"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1016\/j.artint.2015.01.002","volume":"223","author":"A Balint","year":"2015","unstructured":"Balint, A., Belov, A., J\u00e4rvisalo, M., Sinz, C.: Overview and analysis of the SAT Challenge 2012 solver competition. Artif. Intell. 223, 120\u2013155 (2015). https:\/\/doi.org\/10.1016\/j.artint.2015.01.002","journal-title":"Artif. Intell."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M.: SAT Competition 2016: Recent developments. In: Singh, S.P., Markovitch, S. (eds.) Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, San Francisco, California, USA, 4\u20139 February 2017, pp. 5061\u20135063. AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.10641"},{"issue":"3","key":"1_CR7","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s10817-012-9246-5","volume":"50","author":"C Barrett","year":"2013","unstructured":"Barrett, C., Deters, M., de Moura, L., Oliveras, A., Stump, A.: 6 years of SMT-COMP. J. Autom. Reason. 50(3), 243\u2013277 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9246-5","journal-title":"J. Autom. Reason."},{"issue":"4","key":"1_CR8","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1142\/S0218213008004060","volume":"17","author":"C Barrett","year":"2008","unstructured":"Barrett, C., Deters, M., Oliveras, A., Stump, A.: Design and results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-COMP 2007). Int. J. Artif. Intell. Tools 17(4), 569\u2013606 (2008)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"1_CR9","unstructured":"Barrett, C., Deters, M., Oliveras, A., Stump, A.: Design and results of the 4th Annual Satisfiability Modulo Theories Competition (SMT-COMP 2008). Technical report TR2010-931, New York University (2010)"},{"issue":"4","key":"1_CR10","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/s10817-006-9026-1","volume":"35","author":"C Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., Stump, A.: Design and results of the 1st Satisfiability Modulo Theories Competition (SMT-COMP 2005). J. Autom. Reason. 35(4), 373\u2013390 (2005)","journal-title":"J. Autom. Reason."},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10703-007-0038-1","volume":"31","author":"C Barrett","year":"2007","unstructured":"Barrett, C., de Moura, L., Stump, A.: Design and results of the 2nd Annual Satisfiability Modulo Theories Competition (SMT-COMP 2006). Form. Methods Syst. Des. 31, 221\u2013239 (2007)","journal-title":"Form. Methods Syst. Des."},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Bonakdarpour, B., Falcone, Y.: First international competition on software for runtime verification. In: Bonakdarpour, B., Smolka, S.A. (eds.) Proc. of RV 2014: The 5th International Conference on Runtime Verification, LNCS, vol. 8734, pp.\u00a01\u20139. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_1","DOI":"10.1007\/978-3-319-11164-3_1"},{"key":"1_CR13","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10009-017-0454-5","volume":"21","author":"E Bartocci","year":"2019","unstructured":"Bartocci, E., Falcone, Y., Bonakdarpour, B., Colombo, C., Decker, N., Havelund, K., Joshi, Y., Klaedtke, F., Milewicz, R., Reger, G., Rosu, G., Signoles, J., Thoma, D., Zalinescu, E., Zhang, Y.: First international competition on runtime verification: Rules, benchmarks, tools, and final results of CRV 2014. Int. J. Softw. Tools Technol. Transfer 21, 31\u201370 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0454-5","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Falcone, Y., Reger, G.: International competition on runtime verification (CRV). In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 41\u201349. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_3","DOI":"10.1007\/978-3-030-17502-3_3"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Berre, D.L., Simon, L.: The essentials of the SAT 2003 Competition. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, Santa Margherita Ligure, Italy, 5\u20138 May 2003, Selected Revised Papers, LNCS, vol.\u00a02919, pp. 452\u2013467. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24605-3_34"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Berre, D.L., Simon, L.: Fifty-five solvers in Vancouver: The SAT 2004 Competition. In: Hoos, H.H., Mitchell, D.G. (eds.) Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, 10\u201313 May 2004, Revised Selected Papers, LNCS, vol.\u00a03542, pp. 321\u2013344. Springer, Heidelberg (2005)","DOI":"10.1007\/11527695_25"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification (SV-COMP). In: Proc. TACAS, LNCS, vol. 7214, pp. 504\u2013524. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_38","DOI":"10.1007\/978-3-642-28756-5_38"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Second competition on software verification (Summary of SV-COMP 2013). In: Proc. TACAS, LNCS, vol. 7795, pp. 594\u2013609. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_43","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Status report on software verification (Competition summary SV-COMP 2014). In: Proc. TACAS, LNCS, vol. 8413, pp. 373\u2013388. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_25","DOI":"10.1007\/978-3-642-54862-8_25"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Software verification and verifiable witnesses (Report on SV-COMP 2015). In: Proc. TACAS, LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_31","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (Report on SV-COMP 2016). In: Proc. TACAS, LNCS, vol. 9636, pp. 887\u2013904. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_55","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Software verification with validation of results (Report on SV-COMP 2017). In: Proc. TACAS, LNCS, vol. 10206, pp. 331\u2013349. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_20","DOI":"10.1007\/978-3-662-54580-5_20"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Automatic verification of C and Java programs: SV-COMP 2019. In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 133\u2013155. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_9","DOI":"10.1007\/978-3-030-17502-3_9"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Beyer, D.: International competition on software testing (Test-Comp). In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 167\u2013175. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_11","DOI":"10.1007\/978-3-030-17502-3_11"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: Exchanging verification results between verifiers. In: Proc. FSE, pp. 326\u2013337. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Proc. FSE, pp. 721\u2013733. ACM (2015). https:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Beyer, D., Huisman, M., Klebanov, V., Monahan, R.: Evaluating software verification systems: Benchmarks and competitions (Dagstuhl reports 14171). Dagstuhl Rep. 4(4), 1\u201319 (2014). https:\/\/doi.org\/10.4230\/DagRep.4.4.1","DOI":"10.4230\/DagRep.4.4.1"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Software verification: Testing vs. model checking. In: Proc. HVC, LNCS, vol. 10629, pp. 99\u2013114. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_7","DOI":"10.1007\/978-3-319-70389-3_7"},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y , https:\/\/www.sosy-lab.org\/research\/pub\/2019-STTT.Reliable_Benchmarking_Requirements_and_Solutions.pdf","DOI":"10.1007\/s10009-017-0469-y"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wendler, P.: Reuse of verification results: Conditional model checking, precision reuse, and verification witnesses. In: Proc. SPIN, LNCS, vol. 7976, pp. 1\u201317. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39176-7_1","DOI":"10.1007\/978-3-642-39176-7_1"},{"issue":"5","key":"1_CR31","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s10009-014-0334-1","volume":"16","author":"D Beyer","year":"2014","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software verification. Int. J. Softw. Tools Technol. Transfer 16(5), 507\u2013518 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Bormer, T., Brockschmidt, M., Distefano, D., Ernst, G., Filli\u00e2tre, J.C., Grigore, R., Huisman, M., Klebanov, V., March\u00e9, C., Monahan, R., Mostowski, W., Polikarpova, N., Scheben, C., Schellhorn, G., Tofan, B., Tschannen, J., Ulbrich, M.: The COST IC0701 verification competition 2011. In: Beckert, B., Damiani, F., Gurov, D. (eds.) International Conference on Formal Verification of Object-Oriented Systems (FoVeOOS 2011), LNCS, vol.\u00a07421, pp. 3\u201321. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-31762-0_2"},{"key":"1_CR33","unstructured":"Cok, D.R., D\u00e9harbe, D., Weber, T.: The 2014 SMT competition. J. Satisf. Boolean Model. Comput. 9, 207\u2013242 (2014). https:\/\/satassociation.org\/jsat\/index.php\/jsat\/article\/view\/122"},{"key":"1_CR34","unstructured":"Cok, D.R., Griggio, A., Bruttomesso, R., Deters, M.: The 2012 SMT Competition (2012). http:\/\/smtcomp.sourceforge.net\/2012\/reports\/SMTCOMP2012.pdf"},{"issue":"1","key":"1_CR35","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10817-015-9328-2","volume":"55","author":"DR Cok","year":"2015","unstructured":"Cok, D.R., Stump, A., Weber, T.: The 2013 evaluation of SMT-COMP and SMT-LIB. J. Autom. Reason. 55(1), 61\u201390 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9328-2","journal-title":"J. Autom. Reason."},{"issue":"4","key":"1_CR36","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.entcs.2007.06.018","volume":"176","author":"G Denker","year":"2007","unstructured":"Denker, G., Talcott, C.L., Rosu, G., van den Brand, M., Eker, S., Serbanuta, T.F.: Rewriting logic systems. Electron. Notes Theor. Comput. Sci. 176(4), 233\u2013247 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2007.06.018","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Garavel, H.: The rewrite engines competitions: A RECtrospective. In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 93\u2013100. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_6","DOI":"10.1007\/978-3-030-17502-3_6"},{"key":"1_CR38","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., Rold\u00e1n, M., Bach, J.C., Balland, E., van\u00a0den Brand, M., Cordy, J.R., Eker, S., Engelen, L., de\u00a0Jonge, M., Kalleberg, K.T., Kats, L.C.L., Moreau, P.E., Visser, E.: The third Rewrite Engines Competition. In: \u00d6lveczky, P.C. (ed.) Proceedings of the 8th International Workshop on Rewriting Logic and Its Applications (WRLA 2010), Paphos, Cyprus, LNCS, vol.\u00a06381, pp. 243\u2013261. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16310-4_16","DOI":"10.1007\/978-3-642-16310-4_16"},{"issue":"3","key":"1_CR39","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.entcs.2009.05.025","volume":"238","author":"F Dur\u00e1n","year":"2009","unstructured":"Dur\u00e1n, F., Rold\u00e1n, M., Balland, E., van den Brand, M., Eker, S., Kalleberg, K.T., Kats, L.C.L., Moreau, P.E., Schevchenko, R., Visser, E.: The second Rewrite Engines Competition. Electron. Notes Theor. Comput. Sci. 238(3), 281\u2013291 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.05.025","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Ernst, G., Huisman, M., Mostowski, W., Ulbrich, M.: VerifyThis \u2013 verification competition with a human factor. In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 176\u2013195. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_12","DOI":"10.1007\/978-3-030-17502-3_12"},{"key":"1_CR41","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Nickovic, D., Reger, G., Thoma, D.: Second international competition on runtime verification CRV 2015. In: Proc. of RV 2015: The 6th International Conference on Runtime Verification, LNCS, vol.\u00a09333, pp. 405\u2013422. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3","DOI":"10.1007\/978-3-319-23820-3"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Garavel, H., Tabikh, M.A., Arrada, I.S.: Benchmarking implementations of term rewriting and pattern matching in algebraic, functional, and object-oriented languages \u2013 The 4th Rewrite Engines Competition. In: Rusu, V. (ed.) Proceedings of the 12th International Workshop on Rewriting Logic and Its Applications (WRLA 2018), Thessaloniki, Greece, LNCS, vol. 11152, pp. 1\u201325. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99840-4_1","DOI":"10.1007\/978-3-319-99840-4_1"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Geske, M., Isberner, M., Steffen, B.: Rigorous examination of reactive systems. In: Bartocci, E., Majumdar, R. (eds.) Runtime Verification (2015)","DOI":"10.1007\/978-3-319-23820-3_28"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., van de Pol, J.: RERS 2016: Parallel and sequential benchmarks with focus on LTL verification. In: ISoLA, LNCS, vol. 9953, pp. 787\u2013803. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-47169-3_59"},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"Giesl, J., Mesnard, F., Rubio, A., Thiemann, R., Waldmann, J.: Termination competition (termCOMP 2015). In: Felty, A., Middeldorp, A. (eds.) CADE-25, LNCS, vol. 9195, pp. 105\u2013108. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_6","DOI":"10.1007\/978-3-319-21401-6_6"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 156\u2013166. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J., K\u0159et\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Ruijters, E., Steinmetz, M.: The 2019 comparison of tools for the analysis of quantitative formal models. In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 69\u201392. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_5","DOI":"10.1007\/978-3-030-17502-3_5"},{"key":"1_CR48","doi-asserted-by":"publisher","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: Analysis of event-condition-action systems. In: Proc. ISoLA, pp. 608\u2013614, LNCS, vol. 7609, pp. 608\u2013614. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34026-0_45","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"1_CR49","doi-asserted-by":"publisher","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., P\u0103s\u0103reanu, C.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. STTT 16(5), 457\u2013464 (2014). https:\/\/doi.org\/10.1007\/s10009-014-0337-y","DOI":"10.1007\/s10009-014-0337-y"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Howar, F., Steffen, B., Merten, M.: From ZULU to RERS. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation, LNCS, vol. 6415, pp. 687\u2013704. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-16558-0_55"},{"key":"1_CR51","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis verification competition 2012 \u2013 organizer\u2019s report. Technical report 2013-01, Department of Informatics, Karlsruhe Institute of Technology (2013). http:\/\/digbib.ubka.uni-karlsruhe.de\/volltexte\/1000034373"},{"key":"1_CR52","unstructured":"Huisman, M., Monahan, R., Mostowski, W., M\u00fcller, P., Ulbrich, M.: VerifyThis 2017: A program verification competition. Technical report, Karlsruhe Reports in Informatics (2017)"},{"key":"1_CR53","unstructured":"Huisman, M., Monahan, R., M\u00fcller, P., Paskevich, A., Ernst, G.: VerifyThis 2018: A program verification competition. Technical report, Inria (2019)"},{"key":"1_CR54","unstructured":"Huisman, M., Monahan, R., M\u00fcller, P., Poll, E.: VerifyThis 2016: A program verification competition. Technical report TR-CTIT-16-07, Centre for Telematics and Information Technology, University of Twente, Enschede (2016)"},{"issue":"6","key":"1_CR55","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10009-015-0396-8","volume":"17","author":"M Huisman","year":"2015","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis 2012. Int. J. Softw. Tools Technol. Transf. 17(6), 647\u2013657 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"6","key":"1_CR56","doi-asserted-by":"publisher","first-page":"763","DOI":"10.1007\/s10009-016-0438-x","volume":"19","author":"M Huisman","year":"2017","unstructured":"Huisman, M., Klebanov, V., Monahan, R., Tautschnig, M.: VerifyThis 2015. A program verification competition. Int. J. Softw. Tools Technol. Transf. 19(6), 763\u2013771 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR57","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Bloem, R., Brenguier, R., Ehlers, R., Hell, T., K\u00f6nighofer, R., P\u00e9rez, G.A., Raskin, J., Ryzhyk, L., Sankur, O., Seidl, M., Tentrup, L., Walker, A.: The first reactive synthesis competition (SYNTCOMP 2014). STTT 19(3), 367\u2013390 (2017). https:\/\/doi.org\/10.1007\/s10009-016-0416-3","DOI":"10.1007\/s10009-016-0416-3"},{"key":"1_CR58","doi-asserted-by":"publisher","unstructured":"J\u00e4rvisalo, M., Berre, D.L., Roussel, O., Simon, L.: The international SAT solver competitions. AI Mag. 33(1) (2012). https:\/\/doi.org\/10.1609\/aimag.v33i1.2395","DOI":"10.1609\/aimag.v33i1.2395"},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"Jasper, M., Fecke, M., Steffen, B., Schordan, M., Meijer, J., Pol, J.v.d., Howar, F., Siegel, S.F.: The RERS 2017 Challenge and Workshop (invited paper). In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, SPIN 2017, pp. 11\u201320. ACM (2017)","DOI":"10.1145\/3092282.3098206"},{"key":"1_CR60","doi-asserted-by":"crossref","unstructured":"Jasper, M., Mues, M., Murtovi, A., Schl\u00fcter, M., Howar, F., Steffen, B., Schordan, M., Hendriks, D., Schiffelers, R., Kuppens, H., Vaandrager, F.: RERS 2019: Combining synthesis with real-world models. In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 101\u2013115. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_7","DOI":"10.1007\/978-3-030-17502-3_7"},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"Jasper, M., Mues, M., Schl\u00fcter, M., Steffen, B., Howar, F.: RERS 2018: CTL, LTL, and reachability. In: ISoLA 2018, LNCS, vol. 11245, pp. 433\u2013447. Springer, Cham (2018)","DOI":"10.1007\/978-3-030-03421-4_27"},{"key":"1_CR62","doi-asserted-by":"crossref","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: High-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (2015)","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"1_CR63","unstructured":"Klebanov, V., Beckert, B., Biere, A., Sutcliffe, G. (eds.) Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, United Kingdom, 30 June 2012, CEUR Workshop Proceedings, vol. 873. CEUR-WS.org (2012). http:\/\/ceur-ws.org\/Vol-873"},{"key":"1_CR64","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Amparore, E., Beccuti, M., Berthomieu, B., Ciardo, G., Dal Zilio, S., Liebke, T., Linard, A., Meijer, J., Miner, A., Srba, J., Thierry-Mieg, J., van de Pol, J., Wolf, K.: Complete Results for the 2018 Edition of the Model Checking Contest, June 2018. http:\/\/mcc.lip6.fr\/2018\/results.php"},{"key":"1_CR65","doi-asserted-by":"crossref","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Berthomieu, B., Ciardo, G., Colange, M., Dal Zilio, S., Amparore, E., Beccuti, M., Liebke, T., Meijer, J., Miner, A., Rohr, C., Srba, J., Thierry-Mieg, Y., van de Pol, J., Wolf, K.: Complete Results for the 2017 Edition of the Model Checking Contest, June 2017. http:\/\/mcc.lip6.fr\/2017\/results.php","DOI":"10.1007\/978-3-662-58381-4_9"},{"key":"1_CR66","doi-asserted-by":"crossref","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Chiardo, G., Hamez, A., Jezequel, L., Miner, A., Meijer, J., Paviot-Adet, E., Racordon, D., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Tri\u0323nh, G., Wolf, K.: Complete Results for the 2016 Edition of the Model Checking Contest, June 2016. http:\/\/mcc.lip6.fr\/2016\/results.php","DOI":"10.1007\/978-3-662-53401-4_12"},{"key":"1_CR67","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Linard, A., Beccuti, M., Evangelista, S., Hamez, A., Lohmann, N., Lopez, E., Paviot-Adet, E., Rodriguez, C., Rohr, C., Srba, J.: HTML results from the Model Checking Contest @ Petri Net (2014 edition) (2014). http:\/\/mcc.lip6.fr\/2014"},{"key":"1_CR68","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Linard, A., Beccuti, M., Hamez, A., Lopez-Bobeda, E., Jezequel, L., Meijer, J., Paviot-Adet, E., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Wolf, K.: Complete Results for the 2015 Edition of the Model Checking Contest (2015). http:\/\/mcc.lip6.fr\/2015\/results.php"},{"key":"1_CR69","doi-asserted-by":"publisher","unstructured":"Kordon, F., Hulin-Hubard, F.: BenchKit, a tool for massive concurrent benchmarking. In: Proc. ACSD, pp. 159\u2013165. IEEE (2014). https:\/\/doi.org\/10.1109\/ACSD.2014.12","DOI":"10.1109\/ACSD.2014.12"},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"Kordon, F., Linard, A., Buchs, D., Colange, M., Evangelista, S., Lampka, K., Lohmann, N., Paviot-Adet, E., Thierry-Mieg, Y., Wimmel, H.: Report on the model checking contest at Petri Nets 2011. In: Transactions on Petri Nets and Other Models of Concurrency (ToPNoC) VI, LNCS, vol. 7400, pp. 169\u2013196 (2012)","DOI":"10.1007\/978-3-642-35179-2_8"},{"key":"1_CR71","unstructured":"Kordon, F., Linard, A., Beccuti, M., Buchs, D., Fronc, L., Hillah, L., Hulin-Hubard, F., Legond-Aubry, F., Lohmann, N., Marechal, A., Paviot-Adet, E., Pommereau, F., Rodr\u00edguez, C., Rohr, C., Thierry-Mieg, Y., Wimmel, H., Wolf, K.: Model checking contest @ Petri Nets, report on the 2013 edition. CoRR abs\/1309.2485 (2013). http:\/\/arxiv.org\/abs\/1309.2485"},{"key":"1_CR72","unstructured":"Kordon, F., Linard, A., Buchs, D., Colange, M., Evangelista, Fronc, L., Hillah, L.M., Lohmann, N., Paviot-Adet, E., Pommereau, F., Rohr, C., Thierry-Mieg, Y., Wimmel, H., Wolf, K.: Raw report on the model checking contest at Petri Nets 2012. CoRR abs\/1209.2382 (2012). http:\/\/arxiv.org\/abs\/1209.2382"},{"key":"1_CR73","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/j.artint.2016.04.002","volume":"237","author":"F Lonsing","year":"2016","unstructured":"Lonsing, F., Seidl, M., Gelder, A.V.: The QBF gallery: Behind the scenes. Artif. Intell. 237, 92\u2013114 (2016). https:\/\/doi.org\/10.1016\/j.artint.2016.04.002","journal-title":"Artif. Intell."},{"key":"1_CR74","doi-asserted-by":"publisher","unstructured":"March\u00e9, C., Zantema, H.: The termination competition. In: Baader, F. (ed.) Proc. RTA, LNCS, vol. 4533, pp. 303\u2013313. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73449-9_23","DOI":"10.1007\/978-3-540-73449-9_23"},{"key":"1_CR75","doi-asserted-by":"crossref","unstructured":"Meijer, J., van de Pol, J.: Sound black-box checking in the LearnLib. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NASA Formal Methods, LNCS, vol. 10811, pp. 349\u2013366. Springer, Cham (2018)","DOI":"10.1007\/978-3-319-77935-5_24"},{"key":"1_CR76","doi-asserted-by":"crossref","unstructured":"Middeldorp, A., Nagele, J., Shintani, K.: Confluence competition 2019. In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 25\u201340. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_2","DOI":"10.1007\/978-3-030-17502-3_2"},{"issue":"5","key":"1_CR77","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-014-0335-0","volume":"16","author":"J Morse","year":"2014","unstructured":"Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Applying symbolic bounded model checking to the 2012 RERS greybox challenge. Int. J. Softw. Tools Technol. Transfer 16(5), 519\u2013529 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"2\u20133","key":"1_CR78","first-page":"77","volume":"15","author":"R Nieuwenhuis","year":"2002","unstructured":"Nieuwenhuis, R.: The impact of CASC in the development of automated deduction systems. AI Commun. 15(2\u20133), 77\u201378 (2002)","journal-title":"AI Commun."},{"issue":"2\u20133","key":"1_CR79","first-page":"79","volume":"15","author":"F Pelletier","year":"2002","unstructured":"Pelletier, F., Sutcliffe, G., Suttner, C.: The development of CASC. AI Commun. 15(2\u20133), 79\u201390 (2002)","journal-title":"AI Commun."},{"issue":"5","key":"1_CR80","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s10009-014-0324-3","volume":"16","author":"J Pol van de","year":"2014","unstructured":"van de Pol, J., Ruys, T.C., te Brinke, S.: Thoughtful brute-force attack of the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transfer 16(5), 481\u2013491 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1_CR81","doi-asserted-by":"publisher","unstructured":"Reger, G., Hall\u00e9, S., Falcone, Y.: Third international competition on runtime verification - CRV 2016. In: Proc. of RV 2016: The 16th International Conference on Runtime Verification, LNCS, vol. 10012, pp. 21\u201337. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9","DOI":"10.1007\/978-3-319-46982-9"},{"key":"1_CR82","unstructured":"Reger, G., Havelund, K. (eds.) RV-CuBES 2017. An International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, Kalpa Publications in Computing, vol.\u00a03. EasyChair (2017)"},{"issue":"5","key":"1_CR83","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/s10009-014-0338-x","volume":"16","author":"M Schordan","year":"2014","unstructured":"Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transfer 16(5), 493\u2013505 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1_CR84","first-page":"173","volume":"9","author":"M Sighireanu","year":"2014","unstructured":"Sighireanu, M., Cok, D.: Report on SL-COMP 2014. JSAT 9, 173\u2013186 (2014)","journal-title":"JSAT"},{"key":"1_CR85","doi-asserted-by":"crossref","unstructured":"Sighireanu, M., P\u00e9rez, J.A.N., Rybalchenko, A., Gorogiannis, N., Iosif, R., Reynolds, A., Serban, C., Katelaan, J., Matheja, C., Noll, T., Zuleger, F., Chin, W.N., Le, Q.L., Ta, Q.T., Le, T.C., Nguyen, T.T., Khoo, S.C., Cyprian, M., Rogalewicz, A., Vojnar, T., Enea, C., Lengal, O., Gao, C., Wu, Z.: SL-COMP: Competition of solvers for separation logic. In: Proc. TACAS, Part 3, LNCS, vol. 11429, pp. 116\u2013132. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_8","DOI":"10.1007\/978-3-030-17502-3_8"},{"issue":"1","key":"1_CR86","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10472-005-0424-6","volume":"43","author":"L Simon","year":"2005","unstructured":"Simon, L., Berre, D.L., Hirsch, E.A.: The SAT2002 competition. Ann. Math. Artif. Intell. 43(1), 307\u2013342 (2005). https:\/\/doi.org\/10.1007\/s10472-005-0424-6","journal-title":"Ann. Math. Artif. Intell."},{"key":"1_CR87","doi-asserted-by":"crossref","unstructured":"Steffen, B., Jasper, M., Meijer, J., van de Pol, J.: Property-preserving generation of tailored benchmark Petri nets. In: 17th International Conference on Application of Concurrency to System Design (ACSD), pp. 1\u20138, June 2017","DOI":"10.1109\/ACSD.2017.24"},{"issue":"5","key":"1_CR88","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/s10009-014-0339-9","volume":"16","author":"B Steffen","year":"2014","unstructured":"Steffen, B., Howar, F., Isberner, M., Naujokat, S., Margaria, T.: Tailored generation of concurrent benchmarks. STTT 16(5), 543\u2013558 (2014)","journal-title":"STTT"},{"key":"1_CR89","doi-asserted-by":"crossref","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation. In: Model Checking Software - 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, 8\u20139 July 2013. Proceedings, pp. 341\u2013357 (2013)","DOI":"10.1007\/978-3-642-39176-7_21"},{"issue":"5","key":"1_CR90","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s10009-014-0336-z","volume":"16","author":"B Steffen","year":"2014","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Int. J. Softw. Tools Technol. Transfer 16(5), 465\u2013479 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1_CR91","doi-asserted-by":"crossref","unstructured":"Steffen, B., Jasper, M.: Property-preserving parallel decomposition. In: Models, Algorithms, Logics and Tools, LNCS, vol. 10460, pp. 125\u2013145. Springer, Cham (2017)","DOI":"10.1007\/978-3-319-63121-9_7"},{"key":"1_CR92","doi-asserted-by":"publisher","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A\u00a0cross-community infrastructure for logic solving. In: Proc. IJCAR, LNCS, vol. 8562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28","DOI":"10.1007\/978-3-319-08587-6_28"},{"issue":"3","key":"1_CR93","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1006393501098","volume":"24","author":"G Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: The CADE-16 ATP System Competition. J. Autom. Reason. 24(3), 371\u2013396 (2000)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"1_CR94","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1023\/A:1017517027537","volume":"27","author":"G Sutcliffe","year":"2001","unstructured":"Sutcliffe, G.: The CADE-17 ATP System Competition. J. Autom. Reason. 27(3), 227\u2013250 (2001)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"1_CR95","first-page":"33","volume":"18","author":"G Sutcliffe","year":"2005","unstructured":"Sutcliffe, G.: The IJCAR-2004 Automated Theorem Proving Competition. AI Commun. 18(1), 33\u201340 (2005)","journal-title":"AI Commun."},{"issue":"2","key":"1_CR96","first-page":"173","volume":"19","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: The CADE-20 Automated Theorem Proving Competition. AI Commun. 19(2), 173\u2013181 (2006)","journal-title":"AI Commun."},{"issue":"2","key":"1_CR97","first-page":"117","volume":"20","author":"G Sutcliffe","year":"2007","unstructured":"Sutcliffe, G.: The 3rd IJCAR Automated Theorem Proving Competition. AI Commun. 20(2), 117\u2013126 (2007)","journal-title":"AI Commun."},{"issue":"1","key":"1_CR98","first-page":"71","volume":"21","author":"G Sutcliffe","year":"2008","unstructured":"Sutcliffe, G.: The CADE-21 Automated Theorem Proving System Competition. AI Commun. 21(1), 71\u201382 (2008)","journal-title":"AI Commun."},{"issue":"1","key":"1_CR99","doi-asserted-by":"publisher","first-page":"59","DOI":"10.3233\/AIC-2009-0441","volume":"22","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The 4th IJCAR Automated Theorem Proving Competition. AI Commun. 22(1), 59\u201372 (2009)","journal-title":"AI Commun."},{"issue":"1","key":"1_CR100","doi-asserted-by":"publisher","first-page":"47","DOI":"10.3233\/AIC-2010-0469","volume":"23","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The CADE-22 Automated Theorem Proving System Competition - CASC-22. AI Commun. 23(1), 47\u201360 (2010)","journal-title":"AI Commun."},{"issue":"1","key":"1_CR101","doi-asserted-by":"publisher","first-page":"75","DOI":"10.3233\/AIC-2010-0483","volume":"24","author":"G Sutcliffe","year":"2011","unstructured":"Sutcliffe, G.: The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5. AI Commun. 24(1), 75\u201389 (2011)","journal-title":"AI Commun."},{"issue":"1","key":"1_CR102","doi-asserted-by":"publisher","first-page":"49","DOI":"10.3233\/AIC-2012-0512","volume":"25","author":"G Sutcliffe","year":"2012","unstructured":"Sutcliffe, G.: The CADE-23 Automated Theorem Proving System Competition - CASC-23. AI Commun. 25(1), 49\u201363 (2012)","journal-title":"AI Commun."},{"issue":"2","key":"1_CR103","doi-asserted-by":"publisher","first-page":"211","DOI":"10.3233\/AIC-130550","volume":"26","author":"G Sutcliffe","year":"2013","unstructured":"Sutcliffe, G.: The 6th IJCAR Automated Theorem Proving System Competition - CASC-J6. AI Commun. 26(2), 211\u2013223 (2013)","journal-title":"AI Commun."},{"issue":"4","key":"1_CR104","doi-asserted-by":"publisher","first-page":"405","DOI":"10.3233\/AIC-140606","volume":"27","author":"G Sutcliffe","year":"2014","unstructured":"Sutcliffe, G.: The CADE-24 Automated Theorem Proving System Competition - CASC-24. AI Commun. 27(4), 405\u2013416 (2014)","journal-title":"AI Commun."},{"issue":"4","key":"1_CR105","doi-asserted-by":"publisher","first-page":"683","DOI":"10.3233\/AIC-150668","volume":"28","author":"G Sutcliffe","year":"2015","unstructured":"Sutcliffe, G.: The 7th IJCAR Automated Theorem Proving System Competition - CASC-J7. AI Commun. 28(4), 683\u2013692 (2015)","journal-title":"AI Commun."},{"issue":"5","key":"1_CR106","doi-asserted-by":"publisher","first-page":"607","DOI":"10.3233\/AIC-160709","volume":"29","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The 8th IJCAR Automated Theorem Proving System Competition - CASC-J8. AI Commun. 29(5), 607\u2013619 (2016)","journal-title":"AI Commun."},{"issue":"2","key":"1_CR107","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP System Competition - CASC. AI Mag. 37(2), 99\u2013101 (2016)","journal-title":"AI Mag."},{"issue":"6","key":"1_CR108","doi-asserted-by":"publisher","first-page":"419","DOI":"10.3233\/AIC-170744","volume":"30","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The CADE-26 Automated Theorem Proving System Competition - CASC-26. AI Commun. 30(6), 419\u2013432 (2017)","journal-title":"AI Commun."},{"issue":"6","key":"1_CR109","doi-asserted-by":"publisher","first-page":"495","DOI":"10.3233\/AIC-180773","volume":"31","author":"G Sutcliffe","year":"2018","unstructured":"Sutcliffe, G.: The 9th IJCAR Automated Theorem Proving System Competition - CASC-29. AI Commun. 31(6), 495\u2013507 (2018)","journal-title":"AI Commun."},{"issue":"1","key":"1_CR110","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1027302123309","volume":"31","author":"G Sutcliffe","year":"2003","unstructured":"Sutcliffe, G., Suttner, C.: The CADE-18 ATP System Competition. J. Autom. Reason. 31(1), 23\u201332 (2003)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"1_CR111","first-page":"103","volume":"17","author":"G Sutcliffe","year":"2004","unstructured":"Sutcliffe, G., Suttner, C.: The CADE-19 ATP System Competition. AI Commun. 17(3), 103\u2013182 (2004)","journal-title":"AI Commun."},{"issue":"1","key":"1_CR112","first-page":"35","volume":"19","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The State of CASC. AI Commun. 19(1), 35\u201348 (2006)","journal-title":"AI Commun."},{"issue":"3","key":"1_CR113","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1023\/A:1015736313131","volume":"28","author":"G Sutcliffe","year":"2002","unstructured":"Sutcliffe, G., Suttner, C., Pelletier, F.: The IJCAR ATP System Competition. J. Autom. Reason. 28(3), 307\u2013320 (2002)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"1_CR114","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1023\/A:1005824522737","volume":"18","author":"G Sutcliffe","year":"1997","unstructured":"Sutcliffe, G., Suttner, C.: Special Issue: The CADE-13 ATP System Competition. J. Autom. Reason. 18(2), 271\u2013286 (1997)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"1_CR115","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1006285423991","volume":"23","author":"G Sutcliffe","year":"1999","unstructured":"Sutcliffe, G., Suttner, C.: The CADE-15 ATP System Competition. J. Autom. Reason. 23(1), 1\u201323 (1999)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"1_CR116","doi-asserted-by":"publisher","first-page":"423","DOI":"10.3233\/AIC-150691","volume":"29","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G., Urban, J.: The CADE-25 Automated Theorem Proving System Competition - CASC-25. AI Commun. 29(3), 423\u2013433 (2016)","journal-title":"AI Commun."},{"issue":"1","key":"1_CR117","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1023\/A:1006006930186","volume":"21","author":"C Suttner","year":"1998","unstructured":"Suttner, C., Sutcliffe, G.: The CADE-14 ATP System Competition. J. Autom. Reason. 21(1), 99\u2013134 (1998)","journal-title":"J. Autom. Reason."},{"key":"1_CR118","doi-asserted-by":"crossref","unstructured":"Waldmann, J.: Report on the termination competition 2008. In: Proc. of WST (2009)","DOI":"10.1007\/978-3-642-02348-4_1"}],"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-17502-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,15]],"date-time":"2022-09-15T05:51:17Z","timestamp":1663221077000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17502-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030175016","9783030175023"],"references-count":118,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17502-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"4 April 2019","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":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/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":"164","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":"42","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":"8","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":"26% - 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":"13","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":"12 full papers and 11 short papers accepted for TOOLympics and SV-COMP (avg. 4 reviewers\/paper, selected from 43 submissions)","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)"}}]}}