Under-approximating loops in C programs for fast counterexample detection.

Area of Science:

• Computer Science
• Software Engineering
• Formal Methods

Background:

• Software model checkers often struggle to detect counterexamples with deep loops.
• Existing methods can explore numerous spurious and lengthy counterexamples before finding relevant ones.

Purpose of the Study:

• To propose a novel technique for software model checking to efficiently detect deep loop counterexamples.
• To address the weakness of current model checkers in handling deep loops.

Main Methods:

• Constructing auxiliary paths to represent the effect of multiple loop iterations.
• Employing sound under-approximation of loop behavior with respect to bit-vector semantics.
• Developing two quantifier elimination techniques to mitigate performance penalties.
• Integrating loop under-approximation with lazy abstraction and bounded model checking.

Main Results:

• The proposed technique efficiently detects deep counterexamples in C programs.
• Demonstrated effectiveness on buffer overflow benchmarks involving array manipulation.
• Auxiliary paths under-approximate loop behavior soundly, enabling faster bug detection.

Conclusions:

• The new approach significantly improves the efficiency of detecting deep loop errors in software verification.
• Loop under-approximation offers a viable strategy for enhancing model checking capabilities for array-manipulating C programs.