Parallelizing bounded model checking using tunnels over a distributed framework
First Claim
Patent Images
1. 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.
3 Assignments
0 Petitions
Accused Products
Abstract
A system and method for bounded model checking of computer programs includes 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. The sub-problems of the TSR method are partitioned in a distributed environment, where the distributed environment includes at least one master processing unit and at least one client unit. The sub-problems are solved by each client independently of other clients to reduce communication overhead and provide scalability.
8 Citations
19 Claims
-
1. 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. - View Dependent Claims (2, 3, 4, 5, 6, 7)
-
-
8. 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 sub-problems by a master controller to one or more clients controllers; partitioning the sub-problems of the TSR method by a client controller or the master controller in response to a first message from the master controller; and solving the sub-problems by a respective client corresponding to a second message from the master controller, where solving is performed independently of other clients to reduce communication overhead and provide scalability. - View Dependent Claims (9, 10, 11, 12, 13, 14, 15)
-
16. A system for bounded model checking of computer programs, the system comprising:
-
a master controller configured to control communication with one or more client controllers; and a tunneling and slicing-based (TSR) BMC reduction method configured to decompose a computer program into sub-problems, the computer program having at least one reachable property node for bounded model checking (BMC), wherein the one or more client controllers are configured to partition the sub-problems of the TSR method and solve the sub-problems independently of other clients to reduce communication overhead and provide scalability. - View Dependent Claims (17, 18, 19)
-
Specification