Paper Info
Title
Thread-modular verification is cartesian abstract interpretation
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.
Year
DOI
Venue
2006
10.1007/11921240_13
ICTAC
Keywords
DocType
Volume
assume-guarantee style,cartesian product,similar abstraction,cartesian abstract interpretation,successful verification technique,qadeer algorithm,abstraction property,qadeer thread-modular algorithm,abstract interpretation,state space,state explosion problem,thread-modular verification
Conference
4281
ISSN
ISBN
Citations 
0302-9743
3-540-48815-4
13
PageRank 
References 
Authors
0.60
6
3
Name
Order
Citations
PageRank
Alexander Malkis1494.65
Andreas Podelski22760197.87
Andrey Rybalchenko3143968.53