# US 10,503,628 B2 · Interpolation based path reduction method in software model checking > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 10,503,628 B2 - Document ID: US10503628B2 - Status: Granted - Kind: B2 - Application number: 15/912,588 - Filed: 2018-03-06 - Published: 2019-03-28 - Granted: 2019-12-10 - Earliest claimed: 2017-09-28 - Assignees: Xidian University - Applicants: Xidian University - Inventors: Cong Tian; Zhao Duan; Zhenhua Duan - Web page: https://patentgrep.com/patent/US10503628B2 ## CPC - G06F 11/3608: {using formal methods, e.g. model checking, abstract interpretation (theorem proving G06N5/013)} - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## 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. ## Claims ### Claim 1 An interpolation based path reduction in software model checking, comprising: reading a C program, performing grammatical and semantic analysis on the C program, and extracting Control Flow Graph (CFG) from an abstract syntax tree; adding safety interpolation and error interpolation to the CFG and extending the CFG; in a process of generating Abstract Reachability Graph (ARG) according to the CFG, checking, in each state, whether the safety interpolation and the error interpolation are implied by current path formula; wherein the interpolation based path reduction in software model checking further comprises: step 1: generating the CFG according to a program to be verified, and adding 3 attributes for the nodes in the CFG: R interpolation, S interpolation and E interpolation where R interpolation is a reachable constraint for determining the reachability of a state, S interpolation and E interpolation are path specifications for accelerating verification process; adding an attribute W for an edge of the CFG where the value of W for an edge represents the number of branches that have not been traversed in a sub-graph rooted at the node pointed by the edge; step 2: generating the ARG by unwinding the CFG, if a new state s is generated along a path and the R interpolation at s is satisfiable, the state s is reachable, then the traversal of the path along s is continued; otherwise, the state s is unreachable, then the path is terminated and other paths are traversed; for a reachable state s, if the E interpolation at the state s is implied by the path formula corresponding to the path, meaning that there is a real counterexample path to a target state along this state and the program is unsafe; if the S interpolation at the state s is implied, meaning that all the paths starting from this state are safe and there is no need to explore the program along the state s; if the state s is reachable and the E interpolation and S interpolation are not implied, then traversing the path along state s; step 3: if a counterexample path to the target state is found in the process of generating the ARG, then whether the counterexample path is spurious is checked; if the counterexample path is not spurious, the program is unsafe; otherwise, refining the model according to the spurious counterexample, updating the R interpolants, the S interpolants and the E interpolants of the corresponding states, and regenerating the ARG until a real counterexample path is found or no counterexample path exists. ### Claim 2 (depends on 1) The interpolation based path reduction method in software model checking according to claim 1, wherein: if the error interpolation of a predetermined state is implied, there is a real counterexample path in the program and the program is unsafe, then verification is ended; if the safety interpolation is implied, all paths rooted at the state are safe and no traversal is needed such that the traversal paths are reduced; if a spurious counterexample path is found, then the safety interpolation and the error interpolation are computed and updated according to Craig interpolation. ### Claim 3 (depends on 1) The interpolation based path reduction method in software model checking according to claim 1, wherein the step 1 that generates the CFG of the program to be verified and initializes the attributes of the nodes and the edges comprises the following steps: (1) finding a target node in the CFG, and reversely traversing the CFG from the target node, then retaining traversed nodes and edges and removing untraversed nodes and edges; (2) obtaining pruned CFG, initializing the values of the attributes, that is, three kinds of interpolations for each node, when initially traversing the CFG to generate the ARG, an initial value of the R interpolant for each node is {true}; the S interpolant is defined as a two-tuple: (F, Is) where the range of F is {full, half}, and the value of Is is a conjunction consisting of predicates; for a node l, if l has no successor nodes or the S interpolants of all successor nodes are full, which is denoted as f, meaning that all successor nodes of l are traversed, and then the S interpolant at l is also full; otherwise, the S interpolation at l is half, which is denoted as h; the form of F(l) is as follows: F ⁡ ( l ) = { full ⁢ if ⁢ ⁢ l ⁢ ⁢ has ⁢ ⁢ no ⁢ ⁢ successors ⁢ ⁢ or ⁢ ⁢ the ⁢ ⁢ S interpolants ⁢ ⁢ of ⁢ ⁢ all ⁢ ⁢ successors ⁢ ⁢ are ⁢ ⁢ full half ⁢ otherwise if l is an endpoint, the initial value of the S interpolant is (full, true), meaning that the path is safe if the endpoint is reached; if l is the target node, the value of the S interpolant is (full, false), meaning that the path is a counterexample path if the target node is reached; for other nodes, the initial values of the S interpolants are (half true), the form of Is(l) is as follows: I s ⁡ ( l ) = { ( full , false ) if ⁢ ⁢ l ⁢ ⁢ is ⁢ ⁢ the ⁢ ⁢ target ⁢ ⁢ node ( full , true ) if ⁢ ⁢ l ⁢ ⁢ is ⁢ ⁢ the ⁢ ⁢ endpoint ( half , true ) otherwise if l is the target node, the initial value of the E interpolant is true, meaning that the path is a real counterexample; if l is the endpoint, the initial value of the E interpolant is false, meaning that the path is certainly unable to reach the target node; for other nodes, the initial values of the E interpolants are false, initially considered as being unable to reach the target node; for W attribute of each edge, the initial value is ⊥, meaning that the traversal hasn't started where the range of W is {N+, ⊥}, and N+ is a set of positive integers. ### Claim 4 (depends on 1) The interpolation based path reduction method in software model checking according to claim 1, where in the step 2, the W attribute is configured to determine an order of traversing the branch edges, and the S interpolation and the E interpolation are configured to improve efficiency of verification, the step 2 further comprises: (1) obtaining a reachable state s, and producing successor states according to transition relationship of the CFG; if there are multiple possible successor states, determining the order by the values of W of the edges where the priority of the value of W is: (>0)>⊥>0; for some edges that have the same value of W, the order is conducted randomly; for a successor state s, if the state s is unreachable according to the R interpolation, the current path terminates and other paths are explored; if the state s is reachable, checking whether the E interpolant of the state s is false; if the E interpolant of the state s is false, meaning that the successor nodes of s[0] have not been traversed, then the process turns to (2); if the E interpolant of the state s is not false, firstly using SSA principle to assign each variable no more than once to obtain the path formula from the initial state so to s where this path formula is denoted as Pf(s0, . . . , s); then, checking whether the E interpolant of s is implied in Pf(s0, . . . , s) by using a SMT solver; if the E interpolant of s is implied, a real counterexample exists in the program and the program is unsafe, then the verification terminates; otherwise, the process turns to (2); (2) checking whether the S interpolant at s is full interpolant; if the S interpolation at s is not full interpolant, the process turns to (3); if the S interpolation at s is, the path formula from the initial state so to s is obtained, denoted as Pf(s0, . . . , s); then checking whether the S interpolant at s is implied in Pf(s0, . . . , s) by using an SMT solver; if the S interpolation at s is implied, all paths starting with state s are safe and there is no need to traverse, then the current path terminates and other paths are explored; (3) checking whether s is the target state; if s is the target state, a counterexample path is found, then the process turns to step 3; if s is not the target state, further determining whether s is covered by other states; if s is covered by other states, there is no need to explore the current path, and then other paths are explored; if s is not covered by other states, continuing to traverse the current path; (4) if there is a reachable state that has not been traversed, the process turns to (1); otherwise, the program is safe and then the verification terminates. ### Claim 5 (depends on 1) The interpolation based path reduction method in software model checking according to claim 1, wherein an optimization strategy in the step 3 comprises: in the step 1, generating the CFG corresponding to the program, traversing all the CFG and pruning the nodes and edges that cannot reach the target node according to the target node; in the step 3, if a spurious counterexample path exists, the three interpolations and the W value of each edge are computed in a counterexample path; in the step 2, if there are more than one successor states for one state, the traversal order of successor states is determined according to the W values of the edges. ### Claim 6 (depends on 1) The interpolation based path reduction method in software model checking according to claim 1, wherein steps of computing the interpolations and W attribute in the step 3 comprise: 1) when a counterexample path path: is found in the process of generating the ARG, checking whether the path is spurious by using an SMT solver; if path is a real counterexample, the program is unsafe and the verification ends; otherwise, the process turns to 2); 2) for computing the R interpolant, for the state si, 0, and post is ; the new R interpolant is computed by Craig interpolation, Craig(pre, post); the R interpolant of si[0] is formally expressed as: R-Intp(si[0])=R-Intp(si[0])∪Craig(Pf(s0, . . . ,si),Pf(si, . . . ,sn)) where Pf(s0, . . . , si) represents the path formula corresponding to the path from s0 to si; 3) for computing the S interpolation, firstly, a maximal reachable prefix Π= is found, 0, 0, the edges are divided into two categories: branch edge Eb and non-branch edge Ea; (2) generating the path formula corresponding to path, where for e∈Eb, the corresponding formula is replaced by true, and for e∈Ea, generating its corresponding formula and forming a new path formula Pf; (3) searching reversely from the edge en−1, if ei1∈Eb, 0. ### Claim 8 A non-transient computer readable medium containing program instructions for causing a computer to perform a method for model checking path reduction based on interpolation, wherein the method comprising: reading a C program, performing grammatical and semantic analysis on the C program, and extracting Control Flow Graph (CFG) from an abstract syntax tree; adding safety interpolation and error interpolation to the CFG and extending the CFG; in a process of generating Abstract Reachability Graph (ARG) according to the CFG, checking whether the safety interpolation and the error interpolation are implied by current path formula in each state; and further comprising: step 1: generating the CFG according to a program to be verified, and adding 3 attributes for the nodes in the CFG: R interpolation, S interpolation and E interpolation, where R interpolation is a reachable constraint for determining reachability of a state, S interpolation and I interpolation are path specifications for accelerating the verification; adding an attribute W for an edge of the CFG, where the value of W for an edge represents the number of branches that have not been traversed in a sub-graph that is rooted at the node pointed by the edge; step 2: generating the ARG according to the generated CFG: if a new state s is generated along a path and the R interpolation corresponding to s is satisfied, meaning that the state s is reachable, then traversal of the path along the state s is continued; otherwise, the state s is unreachable, then the path is terminated and other paths are traversed; for a reachable state s, if the E interpolation corresponding to the state s is implied by the path formula corresponding to the path, meaning that there is a counterexample path from the state s to a target state and the program is unsafe; if the S interpolation corresponding to the state s is implied, meaning that all the paths starting from this state are safe and there is no need to explore the program along the state s; if the state s is reachable and the E interpolation and S interpolation are not implied, then continuing to traversing the path along state s; step 3: if a counterexample path is found in the process of generating ARG, then checking whether the counterexample path is spurious: if the counter example path is spurious, meaning that the program is unsafe; otherwise, refining the model according to the spurious counterexample, updating the R interpolation, the S interpolation and the E interpolation of the corresponding state, and then regenerating the ARG until a real counterexample path is found or no counterexample paths exist. ### Claim 9 (depends on 8) The non-transient computer-readable medium according to claim 8, wherein: if the error interpolant of a predetermined state is implied, meaning that there is a real counterexample path in the program and the program is unsafe, then verification is ended; if the safety interpolation is implied, meaning that all paths rooted at the state are safe and no traversal is needed such that the traversal paths are reduced; if a spurious counterexample path is found, then the safety interpolation and the error interpolation are computed and updated according to Craig interpolation. ### Claim 10 (depends on 8) The non-transient computer-readable medium according to claim 8, wherein the step 1 that generates the CFG of the program to be verified and initializes the attributes of the node and the edge comprises the following steps: (1) finding a target node in the CFG, reversely traversing the CFG from the target node, and then retaining traversed nodes and edges and removing untraversed nodes and edges; (2) obtaining pruned CFG, and initializing the value of the attributes and three kinds of interpolations for each node; an initial value of the R interpolant for each node is {true} when generating initially the ARG by traversing the CFG; the S interpolant is defined as a two-tuple: (F, Is) where the range of F is {full, half}, the value of Is is a conjunction of predicates: for a node l, if l has no successors or the S interpolants of all successor nodes are full, which is denoted as f, meaning that all successor nodes of l are traversed, and then the S interpolant at l is also full; otherwise, the S interpolation at l is half, which is denoted as h; the form of F(l) is as follows: F ⁡ ( l ) = { full ⁢ if ⁢ ⁢ l ⁢ ⁢ has ⁢ ⁢ no ⁢ ⁢ successors ⁢ ⁢ or ⁢ ⁢ the ⁢ ⁢ S interpolants ⁢ ⁢ of ⁢ ⁢ all ⁢ ⁢ successors ⁢ ⁢ are ⁢ ⁢ full half ⁢ otherwise if l is an endpoint, the initial value of the S interpolant is (full, true), meaning that the path is certainly safe if the endpoint is reached; if l is the target node, the value of the S interpolant is (full, false), meaning that the path is a counterexample path if the target node is reached; for other nodes, the S interpolants are (half true), the form of Is(l) is as follows: I s ⁡ ( l ) = { ( full , false ) if ⁢ ⁢ l ⁢ ⁢ is ⁢ ⁢ the ⁢ ⁢ target ⁢ ⁢ node ( full , true ) if ⁢ ⁢ l ⁢ ⁢ is ⁢ ⁢ the ⁢ ⁢ endpoint ( half , true ) otherwise if l is the target node, the initial value of the E interpolant is true, meaning that the path is certainly a real counterexample; if l is the endpoint, the initial value of the E interpolant is false, meaning that the path is certainly unable to reach the target node; for other nodes, the E interpolants are false, initially considered as being unable to reach the target node; for W attribute of each edge, the initial value is ⊥, meaning that the traversal has not started, where the range of W is {N+, ⊥}, N+ is a set of positive integers. ### Claim 11 (depends on 8) The non-transient computer-readable medium according to claim 8, wherein in the step 2, the W attribute is configured to determine an order of traversing the branch edges, and the S interpolation and the E interpolation are configured to improve efficiency of the verification, further comprising: (1) obtaining a reachable state s′ and producing successor states according to transition relationship of the CFG; if there are multiple possible successors, determining the order by the values of W of the edges where the priority of the value of W of the edge is: (>0)>⊥>0; for the edges that have the same value of W, the selection is conducted randomly: for a successor state s, if the state s is unreachable according to the R interpolation, ending the current path and continuing to traverse other paths; if the state s is reachable, checking whether the E interpolant at the state s is false; if the E interpolant at s is false, meaning that the successor node of s[0] hasn't been traversed, then the next step turns to (2); otherwise, firstly using SSA principle to assign each variable no more than once for obtaining the path formula from the initial state s0 to s where this path formula is denoted as Pf(s0, . . . , s); then, checking whether the E interpolant at s is implied in Pf(s0, . . . , s) by using a solver; if the E interpolant at s is implied, meaning that a real counterexample exists in the program and the program is unsafe, then the verification path terminates; otherwise, turning to (2); (2) checking whether the S interpolant of s is full interpolant; if the S interpolant of s is not full, the next step turns to (3); if the S interpolant of s is, the path formula from the initial state s0 to s is obtained, denoted as Pf(s0, . . . , s); then checking whether the S interpolant of s is implied by Pf(s0, . . . , s) by using a solver; if the S interpolant of s is implied, all paths starting with s are safe and there is no need to traverse, then the current path terminates and continuing to traverse other paths; (3) determining whether s is the target state; if s is the target state, a counterexample path is found, then step 3 is executed; if s is not the target state, further checking whether s is covered by other states; if s is covered by other states, there is no need to explore the current path, then other paths are explored; otherwise, continuing to traverse the current path; (4) if there is a reachable state that has not been traversed, turning to (1); otherwise, the program is safe and then the verification terminates. ### Claim 12 (depends on 8) The non-transient computer-readable medium according to claim 8, wherein an optimization strategy in the step 3 comprises: in the step 1, the CFG of a program is generated, and the nodes and edges that do not reach the target node are pruned; in the step 3, if a spurious counterexample path exists, both of the three interpolants and the W value of each edge are computed; in the step 2, if a state has more than one successors, determining a traversal order of the successor states by the W value. ### Claim 13 (depends on 8) The non-transient computer-readable medium according to claim 8, wherein steps of computing the interpolations and W attribute in the step 3 comprise: 1) in the process of generating the ARG, a counterexample path path: is found; then checking whether the path is spurious by an SMT solver; if the path is not spurious, the program is unsafe and the verification ends; otherwise, turning to 2); 2) computing the R interpolant, for the state si, 0 and post is ; the new R interpolants are computed by Craig interpolation, Craig(pre, post); the update of the R interpolant of si[0] is formally expressed as: R-Intp(si[0])=R-Intp(si[0])∪Craig(Pf(s0, . . . ,si),Pf(si, . . . ,sn)) where Pf(s0, . . . , si) represents the path formula corresponding to the path from s0 to si; 3) for computing the S interpolant, firstly, finding a maximal reachable sequence Π=, 0, 0, the edges are divided into two categories: branch edge Eb and non-branch edge Ea; (2) the path formula is generated, where for e∈Eb, the corresponding formula is replaced by true, and for e∈Ea, its corresponding formula is generated and a new path formula Pf is obtained; (3) searching reversely from the edge en−1, if ei1∈Eb, 0.