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个小组参加了这次竞争,其中包括三个核查挑战,并历时两天的工作。报告分析了参加小组如何应对这些挑战,思考了哪些因素使得核查挑战更适合典型的《核查报告》参与者,并概述了在以人为焦点的竞争中,使用截然不同的核查方法比较小组工作的困难。
相关内容
微信扫码咨询专知VIP会员