×

Parallelizing bounded model checking using tunnels over a distributed framework

  • US 8,504,330 B2
  • Filed: 09/24/2008
  • Issued: 08/06/2013
  • Est. Priority Date: 07/14/2008
  • Status: Expired due to Fees
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.

View all claims
  • 3 Assignments
Timeline View
Assignment View
    ×
    ×