构造循环不变式是程序验证的核心问题之一。主流的循环不变式构造方法通常假设程序中的变量在无限数域上取值，然而程序执行过程中变量都是用有限长度的位向量来表示，无限数域上的循环不变式在有限数域的程序中可能不再是不变式，反之亦然。针对这一问题，本文给出一种基于QBF求解的构造有限数域上循环不变式的方法。该方法可用于构造类型丰富的不变式，包括线性（或多项式）等式（或不等式）不变式，支持加、减、乘、除、移位、位操作等，允许不变式中出现量词。本文也例证了该方法在程序终止性证明、循环上界分析、程序正确性证明等方面的应用价值。

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.