Abstract
Verification of multithreaded programs is difficult. It requires reasoning about state spaces that grow exponentially in the number of concurrent threads. Successful verification techniques based on modular composition of over-approximations of thread behaviors have been designed for this task. These techniques have been traditionally described in assume-guarantee style, which does not admit reasoning about the abstraction properties of the involved compositional argument. Flanagan and Qadeer thread-modular algorithm is a characteristic representative of such techniques. In this paper, we investigate the formalization of this algorithm in the framework of abstract interpretation. We identify the abstraction that the algorithm implements; its definition involves Cartesian products of sets. Our result provides a basis for the systematic study of similar abstractions for dealing with the state explosion problem. As a first step in this direction, our result provides a characterization of a minimal increase in the precision of the Flanagan and Qadeer algorithm that leads to the loss of its polynomial complexity.
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
Birkhoff, G.: Lattice Theory, 3rd edn. Amer. Math. Soc., Providence (1967)
Blanchet, B.: Introduction to Abstract Interpretation, lecture script (2002), http://www.di.ens.fr/~blanchet/absint.pdf
Cousot, P., Cousot, R.: Constructive versions of Tarski’s fixed point theorems. Pacific Journal of Mathematics 82(1) (1979)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th annual ACM symposium on principles of program languages (1979)
Cousot, P.: Partial Completeness of Abstract Fixpoint Checking. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol. 1864, pp. 1–25. Springer, Heidelberg (2000)
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)
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)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Kozen, D.: Lower Bounds for Natural Proof Systems. In: FOCS 1977, pp. 261–262 (1977)
Muchnik, S.S., Jones, N.D.: Program Flow Analysis: Theory and Applications. Prentice-Hall, Inc., Englewood Cliffs, 07632
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Malkis, A., Podelski, A., Rybalchenko, A. (2006). Thread-Modular Verification Is Cartesian Abstract Interpretation. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds) Theoretical Aspects of Computing - ICTAC 2006. ICTAC 2006. Lecture Notes in Computer Science, vol 4281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11921240_13
Download citation
DOI: https://doi.org/10.1007/11921240_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48815-6
Online ISBN: 978-3-540-48816-3
eBook Packages: Computer ScienceComputer Science (R0)