Interpolation based path reduction method in software model checking
US10503628B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Mar 6, 2018 |
| Grant date | Dec 10, 2019 |
| Priority date | — |
| Expiry date | Mar 6, 2038 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3608
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.