Paper Info
Title
Verification-Aided Debugging: An Interactive Web-Service For Exploring Error Witnesses
Abstract
Traditionally, a verification task is considered solved as soon as a property violation or a correctness proof is found. In practice, this is where the actual work starts: Is it just a false alarm? Is the error reproducible? Can the error report later be re-used for bug fixing or regression testing? The advent of exchangeable witnesses is a paradigm shift in verification, from simple answers true and false towards qualitatively more valuable information about the reason for the property violation. This paper explains a convenient web-based toolchain that can be used to answer the above questions. We consider as example application the verification of C programs. Our first component collects witnesses and stores them for later re-use; for example, if the bug is fixed, the witness can be tried once again and should now be rejected, or, if the bug was not scheduled for fixing, the database can later provide the witnesses in case an engineer wants to start fixing the bug. Our second component is a web service that takes as input a witness for the property violation and (re-) validates it, i.e .,it re-plays the witness on the system in order to re-explore the state-space in question. The third component is a web service that continues from the second step by offering an interactive visualization that interconnects the error path, the system's sources, the values on the path (test vectors), and the reachability graph. We evaluated the feasibility of our approach on a large benchmark of verification tasks.
Year
DOI
Venue
2016
10.1007/978-3-319-41540-6_28
COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT II
Field
DocType
Volume
Programming language,False alarm,Computer science,Regression testing,Witness,Theoretical computer science,Interactive visualization,Web service,Toolchain,Debugging,Algorithmic program debugging
Conference
9780
ISSN
Citations 
PageRank 
0302-9743
5
0.43
References 
Authors
9
2
Name
Order
Citations
PageRank
Dirk Beyer11736100.85
Matthias Dangl2604.53