Hits:

Indexed by:期刊论文

Date of Publication:2014-10-01

Journal:Dongbei Daxue Xuebao/Journal of Northeastern University

Included Journals:EI、PKU、ISTIC、Scopus

Volume:35

Page Number:13-18

ISSN No.:10053026

Abstract:The verification of software with a large-scale and complex structure suffers from the explosion of state space, which could lead to low efficiency or even failure. Based on the propery verification of ANSI-C source codes, a method for accelerating software verification was proposed by integrating model checking with theorem proving. Firstly, the program was pruned in light of the asserted properties, and the circular paths were compressed with maximally strong connected components to extract the program backbone. Then, the Hoare theory was used to generate an invariant from the compressed circular nodes, which significantly reduced the length of path encoding. Finally, the verified property could be translated into a SMT first-order predicate logic formula and checked for satisfiability by SMT solver Z3. The experimental results showed that the integrated method substantially improves the efficiency of software verification. ?, 2014, Northeastern University. All right reserved.