Abstract
Thread-modular analysis is an incomplete compositional technique for verifying concurrent systems. The heuristic works rather well when there is limited interaction among system components. In this paper, we develop a refinement algorithm that makes thread-modular model checking complete. Our algorithm refines abstract reachable states by exposing local information through auxiliary variables. The experiments show that our complete thread-modular model checking can outperform other complete compositional reasoning techniques.
This work was supported in part by the Chinese National 973 Plan under grant No. 2010CB328003, the NSF of China under grants No. 60903030, the Tsinghua University Initiative Scientific Research Program.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.: Parameterized Verification with Automatically Computed Inductive Assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221–234. Springer, Heidelberg (2001)
Clarke, E., Emerson, E.: Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Cohen, A., Namjoshi, K.S., Sa’ar, Y.: SPLIT: A Compositional LTL Verifier. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 558–561. Springer, Heidelberg (2010)
Cohen, A., Namjoshi, K.: Local proofs for global safety properties. Formal Methods in System Design 34(2), 104–125 (2009)
Flanagan, C., Qadeer, S.: Thread-Modular Model Checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 213–224. Springer, Heidelberg (2003)
Gu, M., Liu, Q.: Automatic compositional reasoning for multi-thread programs. In: 15th International Conference on Computer Supported Cooperative Work in Design (CSCWD), pp. 175–182 (2011)
Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-Modular Abstraction Refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 262–274. Springer, Heidelberg (2003)
Henzinger, T., Jhala, R., Majumdar, R.: Race checking by context inference. ACM SIGPLAN Notices 39(6), 1–13 (2004)
Jones, C.: Development methods for computer programs including a notion of interference. PhD thesis, Oxford University, June 1981. Printed as: Programming Research Group, Technical Monograph 25 (1981)
Jones, C.: Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 5(4), 596–619 (1983)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering (2), 125–143 (1977)
Malkis, A., Podelski, A., Rybalchenko, A.: Thread-Modular Counterexample-Guided Abstraction Refinement. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 356–372. Springer, Heidelberg (2010)
Misra, J., Chandy, K.: Proofs of networks of processes. IEEE Transactions on Software Engineering (4), 417–426 (1981)
Namjoshi, K.S.: Symmetry and Completeness in the Analysis of Parameterized Systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 299–313. Springer, Heidelberg (2007)
Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM 19(5), 279–285 (1976)
Pnueli, A., Ruah, S., Zuck, L.D.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)
Queille, J., Sifakis, J.: Specification and Verification of Concurrent Systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
SPLIT, http://split.ysaar.net/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meng, W., He, F., Wang, BY., Liu, Q. (2012). Thread-Modular Model Checking with Iterative Refinement. In: Goodloe, A.E., Person, S. (eds) NASA Formal Methods. NFM 2012. Lecture Notes in Computer Science, vol 7226. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28891-3_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-28891-3_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28890-6
Online ISBN: 978-3-642-28891-3
eBook Packages: Computer ScienceComputer Science (R0)