The Boogie verification debugger (tool paper). The Boogie Verification Debugger (BVD) is a tool that lets users explore the potential program errors reported by a deductive program verifier. The user interface is like that of a dynamic debugger, but the debugging happens statically without executing the program. BVD integrates with the program-verification engine Boogie. Just as Boogie supports multiple language front-ends, BVD can work with those front-ends through a plug-in architecture. BVD plugins have been implemented for two state-of-the-art verifiers, VCC and Dafny.
References in zbMATH (referenced in 1 article , 1 standard article )
Showing result 1 of 1.
- Le Goues, Claire; Leino, K.Rustan M.; Moskal, Michał: The Boogie verification debugger (tool paper) (2011)