Accelerating high-level bounded model checking
View Patent ↗An accelerated High-Level Bounded Model Checking method that efficiently extracts high-level information from the model, uses that extracted information to obtain an improved verification model, and applies relevant information on-the-fly to simplify the BMC-problem instances.
1. A computer-implemented method for verifying the correctness of a software program comprising steps of:
by using a computer
generating a sequential model of the software program, said sequential model having a number of reachable control states and data states;
balancing reconvergent control paths in the sequential model by inserting control states with no data operations in said control paths, wherein balancing comprises matching the number of control states in the respective control paths,
generating a transformed model from the sequential model of the software program with one or more balanced reconvergent control paths such that the transformed model has fewer reachable control states for at least one depth, while preserving the correctness property and the total number of reachable control states;
determining statically, for the transformed model, which one(s) of its control states are reachable at each depth of the model;
performing a bounded model checking (BMC) verification on the sequential model using the statically determined control state information as constraints to the BMC;
determining a correctness property of the sequential model; and
outputting an indication of that correctness determination.
2. The computer-implemented method of claim 1 wherein said BMC constraints include a reachable block constraint in which the sequential model includes at a given depth only those control states which are reachable.
3. The computer-implemented method of claim 1 wherein said BMC constraints include a mutual exclusion constraint in which the sequential model includes at a given depth only one reachable control state.
4. The computer-implemented method of claim 1 wherein said BMC constraints include a forward reachable block constraint in which the sequential model includes at a given depth only those reachable control states which are associated with a reachable control state at a greater depth.
5. The computer-implemented method of claim 1 wherein said BMC constraints include a backward reachable block constraint in which the sequential model includes at a given depth only those reachable control states which are reachable from control states at a lesser depth.