Automated Compositional Abstraction Re nement for Concurrent C Programs: A Two-Level Approach Export

@misc{citeulike:3392135, abstract = {The state space explosion problem in model checking remains the chief obstacle to the practical verication of real-world distributed systems. We attempt to address this problem in the context of verifying concurrent (message-passing) C programs against safety specications. More specically, we present a fully automated compositional framework which combines two orthogonal abstraction techniques (operating respectively on data and events) within a counterexample-guided abstraction re nement (CEGAR) scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specication is either established or refuted. Our explicit use of compositionality delays the onset of state space explosion for as long as possible. To our knowledge, this is the rst compositional use of CEGAR in the context of model checking concurrent C programs. We describe our approach in detail, and report on some very encouraging preliminary experimental results obtained with our tool MAGIC. 1}, author = {Chaki, Sagar and Yorav, Karen and Clarke, Edmund}, citeulike-article-id = {3392135}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.3480}, comment = {2段階の抽象化を行ってメモリ使用量を抑える。 1: CEGAR 2: Action-Guided abstraction}, keywords = {2003, blast, concurrent, modelchecking, read, verification}, posted-at = {2008-10-10 03:18:37}, priority = {0}, title = {Automated Compositional Abstraction Re nement for Concurrent C Programs: A Two-Level Approach}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.3480} }

TY - ELEC ID - citeulike:3392135 L3 - citeulike-article-id:3392135 N2 - The state space explosion problem in model checking remains the chief obstacle to the practical verication of real-world distributed systems. We attempt to address this problem in the context of verifying concurrent (message-passing) C programs against safety specications. More specically, we present a fully automated compositional framework which combines two orthogonal abstraction techniques (operating respectively on data and events) within a counterexample-guided abstraction re nement (CEGAR) scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specication is either established or refuted. Our explicit use of compositionality delays the onset of state space explosion for as long as possible. To our knowledge, this is the rst compositional use of CEGAR in the context of model checking concurrent C programs. We describe our approach in detail, and report on some very encouraging preliminary experimental results obtained with our tool MAGIC. 1 TI - Automated Compositional Abstraction Re nement for Concurrent C Programs: A Two-Level Approach KW - 2003 KW - blast KW - concurrent KW - modelchecking KW - read KW - verification N1 - 2段階の抽象化を行ってメモリ使用量を抑える。 1: CEGAR 2: Action-Guided abstraction AU - Chaki, Sagar AU - Yorav, Karen AU - Clarke, Edmund UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.3480 ER -