| 摘要 |
Validity of one or more assertions for any concurrent execution of a plurality of software instructions with at most k-1 context switches can be determined. Validity checking can account for execution of the software instructions in an unbounded stack depth scenario. A finite data domain representation can be used. The software instructions can be represented by a pushdown system. Validity checking can account for thread creation during execution of the plurality of software instructions.
|
