QuickInv: Program Invariant Discovery from Execution Traces

Abstract

Automatic loop invariant inference is a fundamental problem in program verification, yet it is challenging due to the complex behavior of program loops, and the problem is undecidable. Traditional approaches are often limited by predefined templates or are specialized to specific types of loop invariants. This thesis presents QuickInv, a dynamic invariant discovery system that is built upon the principles of theory exploration to overcome these limitations. QuickInv discovers high-level invariants by systematically exploring potential invariants by testing against recorded execution traces. We demonstrate QuickInv on several common array programs, such as binary search, selection sort, and merge sort, successfully recovering many key loop invariants.