WingNews logo WingNews
top | item 40364512

(no title)

bennofs | 1 year ago

Yes, that is a limitation. But this limitation is not too bad.

In many cases, a bug in the translation simply makes the proof impossible. Somebody then investigates why the proof does not go through and finds the bug in the translation.

We only have a problem if the bug in the translation specificially cancels a bug in the original code. If there is no systematic risk, it is quite unlikely that two bugs cancel each other in this way.

discuss

order

im3w1l|1 year ago

Let's say you want to check if use after free can ever occur. Your translation is bugged and translates the whole program to a single "nop". Then the verifier happily asserts that the translated program does not cause use after free.

I doubt the translation would be that bad but it could have more subtle issues of the same kind.

bennofs|1 year ago

My argument is that you typically also check other properties, like properties describing what your program should do. These other properties likely wouldn't be satisfied by a nop program, and hopefully the same is true for many subtle issues.