Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








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

URL of the conference:


URL for downloading the paper:

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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section