论文标题
验证2019年：计划验证竞赛（扩展报告）
VerifyThis 2019: A Program Verification Competition (Extended Report)
论文作者
论文摘要
验证这是一系列强调人类方面的程序验证竞赛：参与者应对详细行为属性的验证 - 这超出了全自动验证的能力，而是需要人类专业知识来适当地编码程序，规格和不变。本文介绍了第八版《验证》，该版本在布拉格的ETAPS 2019举行。 13支球队参加了比赛，其中包括三个验证挑战，并跨越了两天的工作。该报告分析了参与团队如何应对这些挑战，反映了什么使验证挑战或多或少适合典型验证的参与者，并概述了使用以人类方面为重点的竞赛中使用巨大不同验证方法比较团队的工作的困难。
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.
