Automatic Error Localization for Software using Deductive Verification
This addresses the frustrating task of error localization for programmers using deductive verification, though it appears incremental as an extended version of prior work.
The paper tackles the problem of automatically locating errors in software after verification detects them, presenting an approach that identifies potential error locations by finding code expressions that can be modified to satisfy specifications. It implements this in the Frama-C framework and provides initial experimental results.
Even competent programmers make mistakes. Automatic verification can detect errors, but leaves the frustrating task of finding the erroneous line of code to the user. This paper presents an automatic approach for identifying potential error locations in software. It is based on a deductive verification engine, which detects errors in functions annotated with pre- and post-conditions. Using an automatic theorem prover, our approach finds expressions in the code that can be modified such that the program satisfies its specification. Scalability is achieved by analyzing each function in isolation. We have implemented our approach in the widely used Frama-C framework and present first experimental results. This is an extended version of [8], featuring an additional appendix.