Documentation of BVD

Apr 10, 2013 at 2:55 PM
any help about documentation..

Apr 16, 2013 at 12:20 AM
I recommend starting with the following BVD paper, "The Boogie Verification Debugger".

Apr 16, 2013 at 12:54 AM

many thanks ! i already read that paper, but couldn't understand that "how to figure out the failing condition" , in particular how the values on different states in the program can help us to verify the program (as BVD is showing the memory values in different states of the program).

many thanks in advance !
Apr 16, 2013 at 1:04 AM
Have you ever used a dynamic debugger to figure out what's going wrong with the execution of a program? BVD is a bit similar. Do not expect it to explicitly advise you on how you must change your program to make it correct. Rather, think of it as dreaming up a counterexample to the correctness of your program and showing you that counterexample, and your job is then to prevent the verifier from thinking about this counterexample, either by fixing your program to render the counterexample impossible or to strengthen your specifications (typically, a loop invariant or a precondition) to constrain the verifier's dreams.

Perhaps you'll find the Dafny Guide useful in explaining how the verifier deals with loops and recursion.