点击次数：

论文类型：期刊论文

发表时间：2014-10-01

发表刊物：Dongbei Daxue Xuebao/Journal of Northeastern University

收录刊物：EI、PKU、ISTIC、Scopus

卷号：35

页面范围：13-18

ISSN号：10053026

摘要：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.