摘要：三种不同的面向对象程序验证器：Gobra，KeY和Dafny。我们展示了通过使用幽灵变量声明和非终止代码的简单技巧，这三种验证器都可以被证明为错误。这表明，这些语言的验证器可能在不费吹灰之力的情况下产生不可靠的结果，并且这种情况可能普遍存在于所有的面向对象验证器中。
作者：Jaymon Furniss
论文ID：2212.02605
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-12-07
PDF 下载： 英文版 中文版pdf翻译中