Model Checking of Multi Threaded Software
AssigneeNEC Laboratories America, Inc.
InventorsVineet Kahlon, Aarti Gupta
Life of this patent
Estimating the term…
Abstract
A technique for model checking of multi-threaded software is herein disclosed which advantageously can be used to verify correctness properties expressed using temporal logic, e.g., linear time temporal logic and branching time temporal logic. The model checking problem of a concurrent system is decomposed into a plurality of model checking problems on individual threads of the multi-threaded software.
Claims20
A method for model checking of multi-threaded software for a correctness property, comprising:
- modeling the multi-threaded software as a concurrent system of pushdown systems communicating using nested locks, each thread modeled as a pushdown system;
- decomposing model checking of the concurrent system for the correctness property into a plurality of model checking problems on individual threads of the multi-threaded software;
- and
- merging results from the plurality of model checking problems into a general result for the concurrent system.
A method for model checking of multi-threaded software for a correctness property, comprising:
- modeling the multi-threaded software as a concurrent system of pushdown systems communicating using nested locks, each thread modeled as a pushdown system;
- constructing an automaton for the correctness property;
- constructing a product automaton for the automaton and for the concurrent system of pushdown systems;
- and
- determining whether there is an acceptance path in the product automaton for the correctness property by decomposing computation of predecessor sets of regular sets of configurations of the concurrent system of pushdown systems into computations of predecessor sets of regular sets of configurations for individual threads.
A method for model checking of multi-threaded software for a correctness property, comprising:
- constructing an automaton from a model of the multi-threaded software and the correctness property;
- and
- decomposing a search for an acceptance path in the automaton into multiple instances of reachability problems across individual threads in the model of the multi-threaded software.
Dependencies are inferred from the claim text.