1. 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.