首页>
外国专利>
Interpolation based path reduction method in software model checking
Interpolation based path reduction method in software model checking
展开▼
机译：软件模型检查中基于插值的路径约简方法
展开▼
页面导航
摘要
著录项
相似文献
摘要
A method for model checking path reduction based on interpolation comprises: reading a C program, performing grammatical and semantic analysis on the C program, and extracting CFG from an abstract syntax tree; adding safety (S) interpolation and error (E) interpolation to the CFG and extending the CFG; in a process of generating ARG according to the CFG, determining, in each state, whether the safety interpolation and the error interpolation are implied by current path formula. The method improves the verification efficiency by computing the S interpolation and the E interpolation, which makes the algorithm of the model checking a better use in large-scale programs. The S interpolation can be used to avoid the unnecessary traversal, greatly reducing the number of ARG state. The E interpolation can be used to quickly determine whether there is a true counterexample in the program, accelerating the program's verification and improving the efficiency.
展开▼
