Patent ID: 7779382

Claim:
One or more computer-readable media having computer-executable instructions for performing a method comprising: receiving a representation of a plurality of software instructions of a multi-threaded program; constructing a pushdown system representation of the plurality of software instructions, the pushdown system modeling a plurality of threads subject to context switches, the pushdown system also modeling at least one thread representative of one or more threads not subject to context switches; and determining validity of one or more assertions for any concurrent execution of the plurality of software instructions having at most k−1 context switches, wherein k is a bounded positive value, wherein the determining validity of the one or more assertions accounts for execution of the software instructions in an unbounded stack depth scenario, and wherein the determining validity of the one or more assertions is performed for at least a first thread of the modeled plurality of threads and a second thread of the modeled plurality of threads, the first thread configured to execute a first sub-plurality of the plurality of software instructions and the second thread configured to execute a second sub-plurality of the plurality of software instructions, the first sub-plurality of software instructions being separate from the second sub-plurality of software instructions, the first thread being configured to execute the first sub-plurality of the plurality of software instructions concurrently with the second thread's execution of the second sub-plurality of the plurality of software instructions.