@inproceedings{christakis2016integrated,
author = {Christakis, Maria and Leino, Rustan and , Peter Müller and Wüstholz, Valentin},
title = {Integrated Environment for Diagnosing Verification Errors},
booktitle = {22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16)},
year = {2016},
month = {April},
abstract = {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.},
publisher = {Springer},
url = {http://approjects.co.za/?big=en-us/research/publication/integrated-environment-diagnosing-verification-errors/},
pages = {424-441},
}