VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties---something 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 two days of work. The 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.

翻译：这是一系列强调人类方面的程序核查竞赛:参与者处理超出完全自动核查能力范围的详细行为特性的核查问题,要求人的专门知识对程序、规格和变量进行适当编码。本文描述了在布拉格ETAPS 2019 举行的第八版《核查》。13个团队参加了这次由三项核查挑战组成的竞赛,为期两天的工作。报告分析了参与小组如何应对这些挑战,思考了哪些因素使得核查挑战或多或少适合典型的核查参与者,并概述了在以人为焦点的竞争中,使用截然不同的核查方法比较小组的工作的困难。