Proving False in Object-Oriented Verification Programs by Exploiting Non-Termination

TL;DR

This paper demonstrates that three popular object-oriented program verifiers can be made unsound by exploiting non-termination and ghost variables, raising concerns about their reliability.

Contribution

It reveals a simple method to cause false proofs in multiple OO verifiers, highlighting potential widespread unsoundness in such tools.

Findings

All three verifiers can be tricked into proving false

Non-termination can be exploited to break verification soundness

The issue may be common across many object-oriented verifiers

Abstract

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.