| 摘要 |
PROBLEM TO BE SOLVED: To provide a method for tunneling and slicing based bounded model checking (BMC) decomposition to improve efficiency and reduce complexity for computer program verification. SOLUTION: A program is decomposed for bounded model checking (BMC) into subproblems by creating a tunnel based on disjunctive control paths through the program. A reduced BMC sub-problem is obtained using BMC unrolling, while using path constraints imposed by at least one tunnel. For the reachable property node, a quantifier-free formula (QFP) in a decidable subset of first order logic is determined. Satisfiability of the QFP is checked, independently and individually, to determine whether the QFP is satisfiable for the subproblem. The decomposing is continued until a BMC bound is reached. COPYRIGHT: (C)2009,JPO&INPIT
|
