Thread-Modular Model Checking Export

@incollection{citeulike:3321737, abstract = {We present thread-modular model checking, a novel technique for verifying correctness properties of loosely-coupled multithreaded software systems. Thread-modular model checking verifies each thread separately using an automatically inferred environment assumption that abstracts the possible steps of other threads. Separate verification of each thread yields significant space and time savings. Suppose there are n threads, each with a local store of size L, where the threads communicate via a shared global store of size G. If each thread is finite-state (without a stack), the naive model checking algorithm requires O(G. L n ) space, whereas thread-modular model checking requires only O(n.G.(G + L)) space. If each thread has a stack, the general model checking problem is undecidable, but thread-modular model checking terminates in polynomial time.}, author = {Flanagan, Cormac and Qadeer, Shaz}, citeulike-article-id = {3321737}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/3-540-44829-2_14}, doi = {10.1007/3-540-44829-2_14}, journal = {Model Checking Software}, keywords = {2003, abstraction, concurrent, modelchecking, verification}, pages = {624}, posted-at = {2008-09-23 14:29:48}, priority = {2}, title = {Thread-Modular Model Checking}, url = {http://dx.doi.org/10.1007/3-540-44829-2_14}, year = {2003} }

TY - CHAP ID - citeulike:3321737 L3 - citeulike-article-id:3321737 N2 - We present thread-modular model checking, a novel technique for verifying correctness properties of loosely-coupled multithreaded software systems. Thread-modular model checking verifies each thread separately using an automatically inferred environment assumption that abstracts the possible steps of other threads. Separate verification of each thread yields significant space and time savings. Suppose there are n threads, each with a local store of size L, where the threads communicate via a shared global store of size G. If each thread is finite-state (without a stack), the naive model checking algorithm requires O(G. L n ) space, whereas thread-modular model checking requires only O(n.G.(G + L)) space. If each thread has a stack, the general model checking problem is undecidable, but thread-modular model checking terminates in polynomial time. JF - Model Checking Software EP - 624 TI - Thread-Modular Model Checking SP - 624 KW - 2003 KW - abstraction KW - concurrent KW - modelchecking KW - verification AU - Flanagan, Cormac AU - Qadeer, Shaz PY - 2003/// UR - http://dx.doi.org/10.1007/3-540-44829-2_14 ER -