DocumentCode :
2879781
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
fYear :
2009
fDate :
29-31 July 2009
Firstpage :
217
Lastpage :
221
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;
fLanguage :
English
Publisher :
ieee
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
Type :
conf
DOI :
10.1109/TASE.2009.35
Filename :
5198505
Link To Document :
بازگشت