Automatic Error Localization for Software using Deductive Verification

TL;DR

This paper introduces an automatic error localization method for software that leverages deductive verification and theorem proving within the Frama-C framework, enabling scalable identification of potential bug locations.

Contribution

It presents a novel approach combining deductive verification with automatic theorem proving for precise error localization in software functions.

Findings

Successfully implemented in Frama-C

Effective in isolating potential error locations

Scalable analysis by function isolation

Abstract

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.