论文标题
通过利用非终止来证明在面向对象的验证程序中证明虚假的验证程序
Proving False in Object-Oriented Verification Programs by Exploiting Non-Termination
论文作者
论文摘要
我们研究了三个不同的面向对象的程序验证符：Gobra，Key和Dafny。我们证明，可以通过使用带有幽灵变量声明和非终止代码的简单技巧来证明这三个可以证明错误。这表明这些语言的验证者可以在没有太多困难的情况下产生不符合的结果，并且在所有OO验证者中可能很常见。
We looked at three different object-oriented program verifiers: Gobra, KeY, and Dafny. We show that all three can be made to prove false by using a simple trick with ghost variable declaration and non-terminating code. This shows that verifiers for these languages can produce unsound results without much difficulty and that this is possibly common throughout all OO verifiers.
