Synthesis of Precise Error Conditions
The article is currently under review.
Abstract
Fault-detection approaches like testing and formal verification usually identify just one or few error paths when they are tasked to find specification violations of a given software system. This leads to incomplete descriptions of the error situation being handed down from detection to localization and debugging, which is concerned with corrective actions to fix the identified faults. If no complete description of the error can be extrapolated from the one or few reported failing cases, there is a risk that identified faults are not completely addressed in repair and some residual faults (of unknown extent) remain. This paper presents a novel systematic approach to address this issue by finding precise error conditions for input variables. Precise error conditions cover all error-inducing inputs without any inputs that do not induce an error. Our approach employs four key components: an~error-condition generator, a~validator to decide if an error condition is precise or imprecise, a~refinement process, and a~condition pruner. These components collaboratively iterate towards precise error conditions. In addition to the outlined approach, we contribute a thorough evaluation on a large benchmark set, an open-source implementation, and a publicly available reproduction package.
Tool and Reproduction Information
A reproduction package of this work is available on Zenodo (). The implementation of DescribErr is available open source in our GIT repository.
Full Results
The experimental results reported in the paper can be seen in the interactive tables below. You can click on the cells in the status columns to see the corresponding log output and use the respective tabs to show various plots. We offer two kinds of tables:
Research Questions
The following plots show the answers to our research questions:
-
RQ1: Effectiveness of DescribErr & RQ2: Verification Comparison
Despite constituting the first attempt to synthesize precise error conditions for defective programs, DescribErr already succeeds for a substantial number of benchmarks in our evaluation.
-
RQ3: Efficiency of DescribErr (Separate)
-
RQ3: Efficiency of DescribErr (Combined)
-
RQ4: Improvements via Dynamic Likely Invariant Inference