关键词: 程序验证, 循环不变式, 带量词的布尔公式

Abstract:

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.

Key words: program verification;loop Invariant;QBF