Proving False in Object-Oriented Verification Programs by Exploiting Non-Termination
Programming Languages
2022-12-07 v1
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.
Cite
@article{arxiv.2212.02605,
title = {Proving False in Object-Oriented Verification Programs by Exploiting Non-Termination},
author = {Jaymon Furniss},
journal= {arXiv preprint arXiv:2212.02605},
year = {2022}
}
Comments
Unsound 2022 paper