PARALLELIZING BOUNDED MODEL CHECKING USING TUNNELS OVER A DISTRIBUTED FRAMEWORK
First Claim
Patent Images
1. A method for bounded model checking of computer programs, 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.
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.
15 Citations
20 Claims
-
1. A method for bounded model checking of computer programs, 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. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8)
-
9. A method for bounded model checking of computer programs, 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 (10, 11, 12, 13, 14, 15, 16)
-
-
17. A system for bounded model checking of computer programs, 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); the one or more client controllers 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 (18, 19, 20)
-
Specification