PED: Proof-Guided Error Diagnosis by Triangulation of Program Error Causes

Error diagnosis, which is the process of identifying the root causes of bugs in software, is a time-consuming process. In general, it is hard to automate error diagnosis due to the unavailability of a full ldquogoldenrdquo specification of the system behavior in realistic software development. We propose a repair-based proof-guided error diagnosis (PED) framework, that provides a first-line attack to find the root causes of the errors in programs by pin-pointing the possible error-sites (buggy statements), and suggesting possible repair fixes. Our framework does not need a complete system specification. Instead, it automatically ldquominesrdquo partial specifications of the intended program behavior from the proofs obtained by static program analysis for standard safety checkers. It uses these partial specifications along with the multiple error traces provided by a model checker to narrow down the possible error sites. It also exploits inherent correlations among the program statements. To capture common programming mistakes, it directs the search to those statements that could be buggy due to simple copy-paste operations or syntactic mistakes such as using les instead of <. To further improve debugging, it prioritizes the repair solutions. We implemented and integrated the PED tool as a plug-in module to a software verification framework. We show the efficacy of such a framework on public benchmarks.