Proving False in Object Oriented Verification Programs by Exploiting Non-Termination
summary
Three small programs show Gobra, KeY, and Dafny producing proofs of false by hiding non-terminating proofs in ghost variables and then compiling only the terminating remainder. Gobra’s partial-verification accepts a self-recursive postcondition, KeY verifies contracts in isolation letting two methods prove each other via mutual recursion, and Dafny’s lambdas allow an Omega combinator style recursion because lambdas lack decreases clauses. Each exploit yields a terminating caller that violates its declared postcondition despite being proved.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:04Breaking OO verifiers with non-termination
- 3:58First example in GoPro verifier
- 9:44Ghost code and partial verification fail
- 10:07Second example in Key verifier for Java
- 13:38Third example in Daphne verifier
- 19:22Summary
- 19:45Audience questions and discussion
related talks
01h 05mVerifying Infinitely Many Programs at Once
01h 02mLanguage Design meets Verifying Compilers
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
15mOn the Impact of Formal Verification on Software Development
19mPredictable Verification using Intrinsic Definitions
28mGradual Verification: Assuring Software Incrementally
13mDynamiTe: Dynamic Termination and Non-termination Proofs