Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse




Conference Paper

Thread-Modular Verification is Cartesian Abstract Interpretation


Malkis,  Alexander
Programming Logics, MPI for Informatics, Max Planck Society;

Podelski,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

Rybalchenko,  Andrey
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Malkis, A., Podelski, A., & Rybalchenko, A. (2006). Thread-Modular Verification is Cartesian Abstract Interpretation. In Theoretical aspects of computing - ICTAC 2006 : third International Colloquium (pp. 183-197). Berlin, Germany: Springer.

Cite as:
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.