软件验证听起来不像乐趣。它涉及检查一个程序，以确保它没有常见的漏洞。所以一支电脑科学家团队从中发了一个叫做木门的比赛。iPad Puzzle游戏可帮助程序员找到“循环不变”，或正式软件验证的重要组成部分。

在加利福尼亚州梅洛公园的斯里国际智库的团队和圣克鲁兹加州大学都接受了“游戏，”或使用游戏样机制使日常任务更有趣。在这种情况下，拼图游戏将挖掘普通消费者执行验证任务。如果它们是娱乐，他们可以更加警觉和发现更多错误。最重要的是，更广泛的人员将可以访问验证的任务。

“木门游戏利用众包技术来搜索软件计划没有漏洞的证据，”科学科学实验室的计划总监John Murray表示，SRI和Chekof Project的主要调查员（众多人群帮助优化正式验证的紧急知识）。“软件代码被插入到这一参与益智游戏中，玩家通过在岛上的植物行为中发现模式来识别新的植物物种。播放游戏的人越多，正确识别模式，验证了更多的代码，他们将与软件程序的其余部分合作 - 它就像解决了巨大的拼图拼图。“

Xylem Puzzle游戏是SRI项目的一部分，称为Chekofv。它是由美国国防高级研究项目（DARPA）资助的人群采购正式验证计划的一部分。要玩游戏，您不必知道关于软件的任何事情。

游戏在一个名为miraflora的新发现的岛屿。玩家是植物学家，送到岛上的许多不寻常的开花植物。Intrepid Explorer被用于检查植物的“Flinaphase比较器”。使用该设备，玩家在植物上找到花朵的特征之间的数学关系。由于球员社区发现并描述了植物，他们可以看到探索了多少岛屿。游戏也有一个故事情节。

Xylem是Darpa的CSFV程序中的五个电脑游戏之一，可在Verigames网站上提供。

“鲜花的数量实际上是软件循环内变量的值。通过在鲜花之间寻找这些关系，您实际上描述了循环的行为，“吉姆怀特·工程学院计算机科学教授和计算机科学教授和大学Xylem的主要调查员Jim Whitehead。

通常，在软件程序中找到循环不变性是一个需要培训的具有挑战性的任务。

“甚至是计算机科学生甚至是一个艰难的概念，”白头说。“通过将其转换为游戏，它成为一个有基本数学技能的未经训练的人可以做到这一点。”

正式的软件验证并非如此，因为训练有素的人太少了。

“没有足够的专家正式验证正在开发的所有类型的软件，”他说。

Sri International计算机科学实验室主任Patrick Lincoln表示，“Chekofv项目是一个积极的研究计划，以高度创新的方式解决了这些复杂的软件问题。通过使正式的软件验证更可访问和乐趣，更多的人可以通过播放木门游戏来帮助增加世界各地的关键软件的可靠性和安全性。“

UCSC游戏和可玩媒体的大约20名工作人员，研究生和大学生参与了创建游戏。游戏可在Apple iTunes App Store中提供免费，并将在2014年可供Android平板电脑可用。

UCSC和SRI还与CEA的研究人员合作，法国替代能源和原子能委员会（委员会àl'énergieatomique etauxénergies替代品）开发了正式验证过程的工具。