Constructing Program Invariants Based on QBF
LI Zhou-jun · Computer Engineering and Science · 2010
Constructing loop invariants is one of the key problems of program verification. State-of-the-art approaches to invariant generation usually assume that program variables are evaluated over infinite domains such as rational or integer. Actually,during the execution of a program,all variables are expressed using bit-vectors with a limited width and evaluated over finite domains. Many invariants suitable for infinite domains may be invalid in finite domains,and vice versa. This paper proposes an approach based on QBF (Quantified Boolean Formula) to construct invariants for programs whose variables are evaluated over finite domains. It can be used to discover a rich class of invariants including linear (or polynomial) equality (or inequality) invariants involving such operations as addition,multiplication,division,shift,bitwise operation,even quantifiers. And we also exemplify the usefulness of this approach in the termination analysis,the bound analysis and the verification of correctness.