Patent ID: 8504330

Claim:
A method for bounded model checking of computer programs, the method comprising: decomposing a program having at least one reachable property node for bounded model checking (BMC) into sub-problems by employing a tunneling and slicing-based (TSR) BMC reduction method by: assigning the sub-problems of the TSR method in a distributed environment, where the distributed environment includes at least one master processing unit and at least one client unit; and solving the sub-problems by each client independently of other clients to reduce communication overhead and provide scalability, wherein decomposing includes: creating at least one tunnel based on disjunctive control paths through the program; obtaining a reduced BMC sub-problem using BMC unrolling, while using path constraints imposed by the at least one tunnel; for the reachable property node, determining a quantifier-free formula (QFP) in a decidable subset of first order logic; and checking satisfiability of the QFP, independently and individually, to determine whether the QFP is satisfiable for the sub-problem.