MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Cook, Byron
Podelski, Andreas
Rybalchenko, Andrey		dblp
dblp
dblp
Not MPG Author(s):
Cook, Byron
Podelski, Andreas
Editor(s):
Ferrante, Jeanne
McKinley, Kathryn S.		dblp
dblp
Not MPII Editor(s):
Ferrante, Jeanne
McKinley, Kathryn S.
BibTeX cite key*:
Rybalchenko2007PLDI-Threads
Title, Booktitle
Title*:
Proving Thread Termination
Booktitle*:
PLDI'07 : Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation
Event, URLs
Conference URL::
Downloading URL:
http://delivery.acm.org/10.1145/1260000/1250771/p320-cook.pdf?key1=1250771&key2=0694403811&coll=GUIDE&dl=GUIDE&CFID=26915529&CFTOKEN=40823010
Event Address*:
San Diego, CA, USA
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
18 March 2007
Event End Date:
18 March 2007
Publisher
Name*:
ACM
URL:
Address*:
New York, NY, USA
Type:
Vol, No, Year, pp.
Series:
Volume:
Number:
Month:
Pages:
320-330
Year*:
2007
VG Wort Pages:
20
ISBN/ISSN:
978-1-59593-633-2
Sequence Number:
DOI:
10.1145/1250734.1250771
Note, Abstract, ©
(LaTeX) Abstract:
Concurrent programs are often designed such that certain functions executing within critical threads must terminate. Examples of such cases can be found in operating systems, web servers, e-mail clients, etc. Unfortunately, no known automatic program termination prover supports a practical method of proving the termination of threads. In this paper we describe such a procedure. The procedure's scalability is achieved through the use of environment models that abstract away the surrounding threads. The procedure's accuracy is due to a novel method of incrementally constructing environment abstractions. Our method finds the conditions that a thread requires of its environment in order to establish termination by looking at the conditions necessary to prove that certain paths through the thread represent well-founded relations if executed in isolation of the other threads. The paper gives a description of experimental results using an implementation of our procedureon Windows device drivers and adescription of a previously unknown bug found withthe tool.
URL for the Abstract:
http://doi.acm.org/10.1145/1250734.1250771
Download
Access Level:
Internal

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



BibTeX Entry:
@INPROCEEDINGS{Rybalchenko2007PLDI-Threads,
AUTHOR = {Cook, Byron and Podelski, Andreas and Rybalchenko, Andrey},
 EDITOR = {Ferrante, Jeanne and McKinley, Kathryn S.},
 TITLE = {Proving Thread Termination},
 BOOKTITLE = {PLDI'07 : Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation},
 PUBLISHER = {ACM},
 YEAR = {2007},
 PAGES = {320--330},
 ADDRESS = {San Diego, CA, USA},
 ISBN = {978-1-59593-633-2},
 DOI = {10.1145/1250734.1250771},
}

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)
Andrey Rybalchenko		Created
03/19/2007 12:00:18 AM
Revisions
6.
5.
4.
3.
2.		Editor(s)
Uwe Brahm
Uwe Brahm
Christine Kiesel
Christine Kiesel
Christine Kiesel		Edit Dates
2007-07-02 14:49:02
2007-07-02 11:41:39
29.06.2007 09:55:25
29.06.2007 09:54:12
28.06.2007 17:40:54