A program fault may be triggered in a number of ways. This analysis framework attempts to safely characterize all the ways this can happen.
Characterizations have varying degrees of accuracy. For example, in this tiny faulty program:
int main() {
int input = read();
if (input == 42) {
error();
}
}
If I say the program may fail when the input value is 42, the characterization is exact; if I say the program may fail when the input take a value between 40 and 47, the characterization is less accurate; if I say the program may fail for some integer, though this is correct, it is the least accurate.
To compute the bounds on the input space for which the program exhibits faulty behavior, we use a combination of overapproximating analyses and underapproximating analyses. An overapproximating analysis offers safety and scalability, but this comes at the cost of false positives. An underapproximating analysis guarantees that the errors it reaches are actually reachable, but to do so it often sacrifices scalability and/or proofs of correctness. By alternating these two analyses, we try to leverage their strengths and mitigate their weaknesses.
The general idea is to first run an overapproximator. If it claims to have found an error, it must provide some evidence. We use this evidence to guide the underapproximator to the possible error. If the underapproximate affirms that this is a true error, we include its path in the characterization of failures. In either case, we instrument the program to block this path (using assume statements), so that subsequent iterations can explore new program subspaces. The analysis ends when the overapproximator declares the program safe (the instrumented blocking clauses are generalized if no new errors can be found, guaranteeing termination).