通过游戏化推断循环不变量

在当今的现代世界中，软件系统中的错误会产生巨大的成本。提高软件质量的一种有前途的方法是自动软件验证。在此方法中，一个自动化工具试图一次性证明软件的正确性。尽管在这一方向上已经取得了显著的进步，但仍有许多情况下自动化工具会失败。我们特别关注软件验证中一直难以自动化的一个方面：推断出足够强的循环不变量以实现验证。在本文中，我们通过游戏化和众包提出了解决此问题的方法。具体来说，我们介绍了一个谜题游戏，玩家在不知情的情况下找到循环不变量，并且不需要任何软件验证的专业知识。我们通过使用Mechanical Turk用户进行的实验表明，玩家喜欢这个游戏，并且能够解决自动化最先进的工具无法解决的验证任务。