Integrated Environment for Diagnosing Verification Errors - Christakis, Maria; Leino, Rustan, Peter Müller; Wüstholz, Valentin (22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), 2016)
A failed attempt to verify a program’s correctness can result in reports of genuine errors, spurious warnings, and timeouts. The main challenge in debugging a verification failure is to determine whether the complaint is genuine or spurious, and to obtain enough information about the failed verification attempt to debug the error. To help a user with this task, this paper presents an extension of the Dafny IDE that seamlessly integrates the Dafny verifier, a dynamic symbolic execution engine, a verification debugger, and a technique for diagnosing timeouts. The paper also reports on experiments that measure the utility of the combined use of these complementary tools.