Title :
Constructing Program Invariants via Solving QBF
Author :
Chen, Shikun ; Li, Zhoujun ; Li, Mengjun
Author_Institution :
Sch. of Comput. Sci., Nat. Univ. of Defence Technol., Changsha, China
Abstract :
Constructing program invariants is one of the key problems 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.
Keywords :
Boolean algebra; constraint handling; program verification; vectors; QBF; Quantified Boolean Formula; bit vector; constructing program invariant; invariant generation; partial correctness proving; program verification problem; total correctness termination; Arithmetic; Computer science; Educational programs; Hardware; Logic; Polynomials; Software engineering; QBF; program invariants; program verification;
Conference_Titel :
Theoretical Aspects of Software Engineering, 2009. TASE 2009. Third IEEE International Symposium on
Conference_Location :
Tianjin
Print_ISBN :
978-0-7695-3757-3
DOI :
10.1109/TASE.2009.35