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.
CITATION STYLE
Christakis, M., Leino, K. R. M., Müller, P., & Wüstholz, V. (2016). Integrated environment for diagnosing verification errors. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9636, pp. 424–441). Springer Verlag. https://doi.org/10.1007/978-3-662-49674-9_25
Mendeley helps you to discover research relevant for your work.