Constructing Program Invariants via Solving QBF
Constructing program invariants is one of the key prob lems of program verification. A lot of approaches to invariant generation have been reported, and all of these methods assume that program variables are evaluated over infinite domains such as rational or integer. Actually, during the execution of program, all variables are expressed using bit-vectors with limited width and evaluated over finite domains. Many invariants suit for infinite domains may be invalid in finite domains, and vice versa. This paper proposes an approach to construct invariants for program whose variables are evaluated over finite domains. This method translates a program into constraints that are solved using a QBF (Quantified Boolean Formula) solver to yield desired program invariants. It can be used to discover a rich class of invariants including linear (or polynomial) equality (or inequality) invariants involving operations like addition, multiplication, division, shift, bitwise operation, even quantifiers. And we also show how this technique can be used to prove partial correctness, termination and total correctness.
Shikun Chen Zhoujun Li Mengjun Li
School of Computer Science National University of Defence Technology ChangSha, China, 410073 School of Computer BeiHang University Beijing, China, 100083
国际会议
天津
英文
217-221
2009-07-29（万方平台首次上网日期，不代表论文的发表时间）