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 3 articles , 1 standard article )

Showing results 1 to 3 of 3.
Sorted by year (citations)

  1. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  2. Leino, K. Rustan M.; Lucio, Paqui: An assertional proof of the stability and correctness of Natural Mergesort (2015)
  3. Le Goues, Claire; Leino, K. Rustan M.; Moskal, Michał: The Boogie verification debugger (tool paper) (2011) ioport