{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T15:30:36Z","timestamp":1787585436259,"version":"build-2736575974"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2021,5,19]],"date-time":"2021-05-19T00:00:00Z","timestamp":1621382400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,5,19]],"date-time":"2021-05-19T00:00:00Z","timestamp":1621382400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Universit\u00e0 della Svizzera italiana"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties\u2014something that lies beyond the capabilities of fully automatic verification and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned 2 days of work. This report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.<\/jats:p>","DOI":"10.1007\/s10009-021-00619-x","type":"journal-article","created":{"date-parts":[[2021,5,19]],"date-time":"2021-05-19T15:21:03Z","timestamp":1621437663000},"page":"883-893","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["VerifyThis 2019: a program verification competition"],"prefix":"10.1007","volume":"23","author":[{"given":"Claire","family":"Dross","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carlo A","family":"Furia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rosemary","family":"Monahan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,5,19]]},"reference":[{"key":"619_CR1","doi-asserted-by":"crossref","unstructured":"Amighi, A., Blom, S., Huisman, M.: VerCors: A layered approach to practical verification of concurrent software. In: IEEE Computer Society 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP), pp. 495\u2013503. (2016). https:\/\/ieeexplore.ieee.org\/abstract\/document\/7445381","DOI":"10.1109\/PDP.2016.107"},{"key":"619_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer, New York (2004)"},{"issue":"4","key":"619_CR3","first-page":"1","volume":"4","author":"D Beyer","year":"2014","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)","journal-title":"Dagstuhl Rep."},{"key":"619_CR4","doi-asserted-by":"crossref","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: Verification of parallel and concurrent software. In: 13th International Conference on Integrated Formal Methods (IFM), Lecture Notes in Computer Science, vol. 10510, pp. 102\u2013110. Springer (2017)","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"619_CR5","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364. Wroc\u0142aw, Poland (2011). https:\/\/hal.inria.fr\/hal-00790310"},{"key":"619_CR6","doi-asserted-by":"crossref","unstructured":"Bormer, T., Brockschmidt, M., Distefano, D., Ernst, G., Filli\u00e2tre, J., 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: Formal Verification of Object-Oriented Software (FoVeOOS), Lecture Notes in Computer Science, vol. 7421, pp. 3\u201321. Springer (2012)","DOI":"10.1007\/978-3-642-31762-0_2"},{"key":"619_CR7","doi-asserted-by":"crossref","unstructured":"Bunte, O., Groote, J.F., Keiren, J.J.A., Laveaux, M., Neele, T., de\u00a0Vink, E.P., Wesselink, W., Wijs, A., Willemse, T.A.C.: The mCRL2 toolset for analysing concurrent systems \u2013 improvements in expressivity and usability. In: Tools and Algorithms for the Construction and Analysis of Systems (Part II), Lecture Notes in Computer Science, vol. 11428, pp. 21\u201339. Springer (2019)","DOI":"10.1007\/978-3-030-17465-1_2"},{"key":"619_CR8","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Proceedings 1st Workshop on Formal Integrated Development Environment (F-IDE), EPTCS, vol. 149, pp. 79\u201392 (2014)","DOI":"10.4204\/EPTCS.149.8"},{"key":"619_CR9","doi-asserted-by":"crossref","unstructured":"Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 7795, pp. 199\u2013213. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_15"},{"key":"619_CR10","doi-asserted-by":"crossref","unstructured":"Dross, C., Furia, C.A., Huisman, M., Monahan, R., M\u00fcller, P.: VerifyThis 2019: A program verification competition (extended report). arXiv:2008.13610 (2020)","DOI":"10.1007\/s10009-021-00619-x"},{"key":"619_CR11","doi-asserted-by":"crossref","unstructured":"Ernst, G., Huisman, M., Mostowski, W., Ulbrich, M.: VerifyThis \u2013 verification competition with a human factor. In: Tools and Algorithms for the Construction and Analysis of Systems \u2013 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Lecture Notes in Computer Science, vol. 11429, pp. 176\u2013195. Springer (2019)","DOI":"10.1007\/978-3-030-17502-3_12"},{"issue":"6","key":"619_CR12","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: Overview and VerifyThis competition. STTT 17(6), 677\u2013694 (2015)","journal-title":"STTT"},{"key":"619_CR13","unstructured":"Filli\u00e2tre, J., Paskevich, A., Stump, A.: The 2nd verified software competition: Experience report. In: Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, CEUR Workshop Proceedings, vol. 873, pp. 36\u201349. CEUR-WS.org (2012)"},{"key":"619_CR14","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Proceedings of the 22nd European Symposium on Programming (ESOP), Lecture Notes in Computer Science, vol. 7792, pp. 125\u2013128. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"619_CR15","volume-title":"Data Analysis Using Regression and Multilevel\/hierarchical Models","author":"A Gelman","year":"2007","unstructured":"Gelman, A., Hill, J.: Data Analysis Using Regression and Multilevel\/hierarchical Models. Cambridge University Press, Cambridge (2007)"},{"issue":"6","key":"619_CR16","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. Transfer 19(6), 763\u2013771 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"619_CR17","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: On the organisation of program verification competitions. In: Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, CEUR Workshop Proceedings, vol. 873, pp. 50\u201359. CEUR-WS.org (2012)"},{"key":"619_CR18","unstructured":"Huisman, M., Monahan, R., M\u00fcller, P., Paskevich, A., Ernst, G.: VerifyThis 2018: A program verification competition. https:\/\/hal.inria.fr\/hal-01981937\/ (2018). HAL Id: hal-01981937, version 1"},{"key":"619_CR19","unstructured":"Huisman, M., Monahan, R., M\u00fcller, P., Poll, E.: VerifyThis 2016: A program verification competition. http:\/\/hdl.handle.net\/2066\/161349 (2016). CTIT technical report 1381-3625"},{"key":"619_CR20","unstructured":"Huisman, M., Monahan, R., M\u00fcller, P., Mostowski, W., Ulbrich, M.: VerifyThis 2017: A program verification competition. Tech. Rep. 10, Karlsruher Institut f\u00fcr Technologie (KIT) (2017)"},{"key":"619_CR21","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, (2018)","DOI":"10.1017\/S0956796818000151"},{"issue":"3","key":"619_CR22","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Asp. Comput."},{"key":"619_CR23","doi-asserted-by":"crossref","unstructured":"Klebanov, V., M\u00fcller, P., Shankar, N., Leavens, G.T., W\u00fcstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M.A., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Wei\u00df, B.: The 1st verified software competition: Experience report. In: FM 2011: Formal Methods, Lecture Notes in Computer Science, vol. 6664, pp. 154\u2013168. Springer (2011)","DOI":"10.1007\/978-3-642-21437-0_14"},{"issue":"4","key":"619_CR24","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s10817-017-9437-1","volume":"62","author":"P Lammich","year":"2019","unstructured":"Lammich, P.: Refinement to imperative HOL. J. Autom. Reason. 62(4), 481\u2013503 (2019)","journal-title":"J. Autom. Reason."},{"key":"619_CR25","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Verification, Model Checking, and Abstract Interpretation (VMCAI), Lecture Notes in Computer Science, vol. 9583, pp. 41\u201362. Springer (2016)","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"619_CR26","doi-asserted-by":"crossref","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: 21st International Conference on Theorem Proving in Higher Order Logics (TPHOL), Lecture Notes in Computer Science, vol. 5170, pp. 33\u201338. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_7"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00619-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00619-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00619-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,26]],"date-time":"2021-12-26T12:02:58Z","timestamp":1640520178000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00619-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,19]]},"references-count":26,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["619"],"URL":"https:\/\/doi.org\/10.1007\/s10009-021-00619-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,5,19]]},"assertion":[{"value":"6 May 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 May 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}