MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Malkis, Alexander
Podelski, Andreas
Rybalchenko, Andrey		dblp
dblp
dblp
Editor(s):
Barkaoui, Kamel
Cavalcanti, Ana
Cerone, Antonio		dblp
dblp
dblp
Not MPII Editor(s):
Barkaoui, Kamel
Cavalcanti, Ana
Cerone, Antonio
BibTeX cite key*:
malkis2006
Title, Booktitle
Title*:
Thread-Modular Verification is Cartesian Abstract Interpretation
Booktitle*:
Theoretical Aspects of Computing - ICTAC 2006 : Third International Colloquium
Event, URLs
Conference URL::
Downloading URL:
http://www.springerlink.com/content/r15015664qq51577/fulltext.pdf
Event Address*:
Tunis, Tunisia
Language:
English
Event Date*
(no longer used):
Organization:
International University Macau
Event Start Date:
20 November 2006
Event End Date:
24 November 2006
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
4281
Number:
Month:
Pages:
183-197
Year*:
2006
VG Wort Pages:
ISBN/ISSN:
978-3-540-48815-6; 3-540-48815-4
Sequence Number:
DOI:
10.1007/11921240_13
Note, Abstract, ©
(LaTeX) 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.
URL for the Abstract:
http://www.springerlink.com/content/r15015664qq51577/
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
Expert
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:
@INPROCEEDINGS{malkis2006,
AUTHOR = {Malkis, Alexander and Podelski, Andreas and Rybalchenko, Andrey},
 EDITOR = {Barkaoui, Kamel and Cavalcanti, Ana and Cerone, Antonio},
 TITLE = {Thread-Modular Verification is Cartesian Abstract Interpretation},
 BOOKTITLE = {Theoretical Aspects of Computing - ICTAC 2006 : Third International Colloquium},
 PUBLISHER = {Springer},
 YEAR = {2006},
 ORGANIZATION = {International University Macau},
 VOLUME = {4281},
 PAGES = {183--197},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Tunis, Tunisia},
 ISBN = {978-3-540-48815-6},
; ISBN = {3-540-48815-4},
 DOI = {10.1007/11921240_13},
}

Entry last modified by Uwe Brahm, 01/28/2008
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Stephanie Müller		Created
11/13/2006 02:16:53 PM
Revisions
7.
6.
5.
4.
3.		Editor(s)
Uwe Brahm
Uwe Brahm
Uwe Brahm
Uwe Brahm
Uwe Brahm		Edit Dates
2007-07-09 09:45:05
2007-07-09 09:44:48
2007-04-26 16:01:01
2007-04-26 15:54:44
2007-04-26 11:32:05